This work is licensed under the Creative Commons Attribution License. Timed Runtime Monitoring for Multiparty Conversations

Abstract We propose a dynamic verification framework for protocols in real-time distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types, developed with our industrial partners. Drawing from recent work on multi-party session types for real-time interactions, we extend Scribble with clocks, resets, and clock predicates constraining the times in which interactions should occur. We present a timed API for Python to program distributed implementations of Scribble specifications. A dynamic verification framework ensures the safe execution of applications written with our timed API: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timing with respect to the corresponding Scribble spec-ification. The performance of our implementation and its practicability are analysed via benchmarking. Recent work [3] extends Multiparty Session Types (MPSTs) to enable the verification of real-time distributed systems. This timed extension allows to express properties on the causalities of interactions, on the carried datatypes, and on the times in which interactions occur. In this paper, we apply the theory in [3] to implement a toolchain for specification and runtime verification of real-time interactions, and evaluate our prototype implementation via benchmarking. This work is motivated by our collaboration with the Ocean Observatories Initiative (OOI) [13]