[BCD+13] 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 recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored pi-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.

@inproceedings{BocchiCDHY13, volume = {7892}, author = {Laura Bocchi and Tzu-Chun Chen and Romain Demangeon and Kohei Honda and Nobuko Yoshida}, series = {Lecture Notes in Computer Science}, booktitle = {FMOODS/FORTE}, url = {http://www.di.unito.it/~chen/papers/FORTE_2013.pdf}, title = {Monitoring Networks through Multiparty Session Types}, isbn = {978-3-642-38591-9}, tag = {FMOOD/FORTE 2013}, 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 recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored pi-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.}, localfile = {http://www.di.unito.it/~chen/papers/FORTE_2013.pdf}, publisher = {Springer}, year = {2013}, pages = {50-65}, }

BocchiCDHY13 (In proceedings)
Author(s)	Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda and Nobuko Yoshida
Title	« Monitoring Networks through Multiparty Session Types »
In	FMOODS/FORTE
Series	Lecture Notes in Computer Science
Volume	7892
Page(s)	50-65
Year	2013
Publisher	Springer
ISBN number	978-3-642-38591-9
URL	http://www.di.unito.it/~chen/papers/FORTE_2013.pdf