Monitoring Networks through Multiparty Session Types

Bocchi, Laura (2017) Monitoring Networks through Multiparty Session Types. Theoretical Computer Science, 669 . pp. 33-58. ISSN 0304-3975. (doi:https://doi.org/10.1016/j.tcs.2017.02.009) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided)

PDF - Publisher pdf

Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (636kB) Preview
[img]
Preview
PDF - Author's Accepted Manuscript

Creative Commons Licence
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
Download (598kB) Preview
[img]
Preview
PDF - Author's Accepted Manuscript
Restricted to Repository staff only
Contact us about this Publication Download (685kB)
[img]
Official URL
http://dx.doi.org/10.1016/j.tcs.2017.02.009

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.

Item Type: Article
Uncontrolled keywords: Session types; The π-calculus; Dynamic monitoring; Runtime verification; Bisimulation
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Laura Bocchi
Date Deposited: 09 Feb 2017 10:55 UTC
Last Modified: 27 Feb 2018 00:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/60279 (The current URI for this page, for reference purposes)
Bocchi, Laura: https://orcid.org/0000-0002-7177-9395
  • Depositors only (login required):

Downloads

Downloads per month over past year