Monitoring networks through multiparty session types
File(s)
Published version
Author(s)
Bocchi, Laura
Chen, Tzu-Chun
Demangeon, Romain
Honda, Kohei
Yoshida, Nobuko
Type
Report
Abstract
In large-scale distributed infrastructures, applications are realised
through communications among distributed components. The need
for methods for assuring safe interactions in such environments is recognized,
however the existing frameworks, relying on centralised veri cation
or restricted speci cation methods, have limited applicability. This paper
proposes a new theory of monitored -calculus with dynamic usage of
multiparty session types (MPST), o ering a rigorous foundation for safety
assurance of distributed components which asynchronously communicate
through multiparty sessions. Our theory establishes a framework for semantically
precise decentralised run-time enforcement and provides reasoning
principles over monitored distributed applications, which complement
existing static analysis techniques. We introduce asynchrony
through the means of explicit routers and global queues, and propose
novel equivalences between networks, that capture the notion of interface
equivalence, i.e. equating networks o ering the same services to a user.
We illustrate our static-dynamic analysis system with an ATM protocol
as a running example and justify our theory with results: satisfaction
equivalence, local/global safety and transparency, and session delity.
through communications among distributed components. The need
for methods for assuring safe interactions in such environments is recognized,
however the existing frameworks, relying on centralised veri cation
or restricted speci cation methods, have limited applicability. This paper
proposes a new theory of monitored -calculus with dynamic usage of
multiparty session types (MPST), o ering a rigorous foundation for safety
assurance of distributed components which asynchronously communicate
through multiparty sessions. Our theory establishes a framework for semantically
precise decentralised run-time enforcement and provides reasoning
principles over monitored distributed applications, which complement
existing static analysis techniques. We introduce asynchrony
through the means of explicit routers and global queues, and propose
novel equivalences between networks, that capture the notion of interface
equivalence, i.e. equating networks o ering the same services to a user.
We illustrate our static-dynamic analysis system with an ATM protocol
as a running example and justify our theory with results: satisfaction
equivalence, local/global safety and transparency, and session delity.
Date Issued
2013-01-01
Citation
Departmental Technical Report: 13/3, 2013, pp.1-28
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
28
Journal / Book Title
Departmental Technical Report: 13/3
Copyright Statement
© 2013 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
13/3