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

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).