Monitoring Networks through Multiparty Session Types

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 verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored π-calculus with dynamic usage of multiparty session types (MPST), offering 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 offering 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 fidelity.
Document type :
Conference papers
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01213683
Contributor : Lip6 Publications <>
Submitted on : Thursday, April 27, 2017 - 11:38:33 AM
Last modification on : Thursday, April 27, 2017 - 2:43:59 PM
Long-term archiving on : Friday, July 28, 2017 - 12:48:46 PM

File

978-3-642-38592-6_5_Chapter.pd...
Files produced by the author(s)

Identifiers

Citation

Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Nobuko Yoshida, Kohei Honda. Monitoring Networks through Multiparty Session Types. 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.50-65, ⟨10.1007/978-3-642-38592-6_5⟩. ⟨hal-01213683⟩

Share

Metrics

Record views

123

Files downloads

193