Post date: 18-Apr-2017 09:57:37
Upcoming Seminar
Behavioural type-checking of time-sensitive protocols
April 21, 15.00 (Aula F)
Palazzo delle Scienze - Cagliari
Laura Bocchi
University of Kent (UK)
Abstract. 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.
Resources