Behavioural type-checking of time-sensitive protocols

Laura Bocchi

In recent work we have extended multiparty session types (MPST) with a model of time borrowed from Communicating Time Automata (CTA). This allowed us to establish a sound and complete correspondence between timed MPST and a subclass of CTA that satisfies progress. On the basis of this correspondence, we can decide properties on CTA that are undecidable in the general case, such as safety (absence of orphan messages and communication mismatches), progress, non-zenoness and eventual reception of messages sent. I will present decidable conditions for these properties, and give a concrete procedure to build *when possible* global timed MPST from (arbitrary) collections of timed automata, with the guarantee that the resulting global specification is a well-behaved composition.

A long version of the abstract can be found here.