Seminar: Behavioural type-checking of time-sensitive protocols

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

• Laura Bocchi, Julien Lange, Nobuko Yoshida. Meeting Deadlines Together. In Proc. CONCUR 2015.
• Laura Bocchi, Weizhen Yang, Nobuko Yoshida. Timed Multiparty Session Types. In Proc. CONCUR 2014.
• Rumyana Neykova, Laura Bocchi, Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. In Formal Aspects of Computing, 2017.