Skip to Main content Skip to Navigation
Conference papers

Compliance and Subtyping in Timed Session Types

Abstract : We propose an extension of binary session types, to formalise timed communication protocols between two participants at the endpoints of a session. We introduce a decidable compliance relation, which generalises to the timed setting the usual progress-based notion of compliance between untimed session types. We then show a sound and complete technique to decide when a timed session type admits a compliant one, and if so, to construct the least session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results. We exploit our theory to design and implement a message-oriented middleware, where distributed modules with compliant protocols can be dynamically composed, and their communications monitored, so to guarantee safe interactions.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01767334
Contributor : Hal Ifip <>
Submitted on : Monday, April 16, 2018 - 10:19:03 AM
Last modification on : Monday, April 16, 2018 - 10:20:24 AM

File

978-3-319-19195-9_11_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Massimo Bartoletti, Tiziana Cimoli, Maurizio Murgia, Alessandro Podda, Livio Pompianu. Compliance and Subtyping in Timed Session Types. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.161-177, ⟨10.1007/978-3-319-19195-9_11⟩. ⟨hal-01767334⟩

Share

Metrics

Record views

473

Files downloads

271