Timed Runtime Monitoring for Multiparty Conversations
This work addresses the need for reliable timing in multiparty conversations for distributed systems, representing an incremental improvement to existing session type tools.
The paper tackles the problem of verifying real-time distributed protocols by extending Scribble with timed constraints and providing a Python API, resulting in a dynamic verification framework that ensures safe execution with runtime monitors.
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.