News‎ > ‎

Seminar: Compliance and subtyping in timed session types

posted Sep 2, 2015, 8:36 AM by Massimo Bartoletti   [ updated Sep 2, 2015, 9:37 AM ]
Upcoming Seminar

Compliance and subtyping in timed session types

September 7, 15.45 (Aula F)
Palazzo delle Scienze - Cagliari

Maurizio Murgia
Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari

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.