Timed session types

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.

Online resources

• M. Bartoletti, T. Cimoli, M. Murgia, L. Pompianu, A.S. Podda. Compliance and subtyping in timed session types. Accepted for publication in FORTE 2015.
• TST compliance checker
• TST dual construction
• CO2 middleware

Acknowledgements

This research has been partially supported by the following projects:

• Autonomous Region of Sardinia grant L.R.7/2007 CRP-17285 TRICS
• Autonomous Region of Sardinia P.I.A. 2010 Social Glue
• MIUR PRIN 2010-11 project Security Horizons
• EU COST Action IC1201 "Behavioural Types for Reliable Large-Scale Software Systems" (BETTY).