Timed Runtime Monitoring for Multiparty Conversations

Rumyana Neykova
(Imperial College London)
Laura Bocchi
(Imperial College London)
Nobuko Yoshida
(Imperial College London)

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 multiparty 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 specification. The performance of our implementation and its practicability are analysed via benchmarking.

In Marco Carbone: Proceedings Third Workshop on Behavioural Types (BEAT 2014), Rome, Italy, 1st September 2014, Electronic Proceedings in Theoretical Computer Science 162, pp. 19–26.
Published: 24th August 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.162.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org