Timed Runtime Monitoring for Multiparty Conversations

TL;DR

This paper introduces a dynamic verification framework for real-time distributed protocols, extending Scribble with timing features and providing runtime monitors to ensure correct interaction timings in multiparty conversations.

Contribution

It extends Scribble with clocks and predicates for real-time verification and develops a timed API with runtime monitors for safe distributed execution.

Findings

Benchmarking shows practical performance of the runtime monitors.

The framework effectively enforces timing constraints in multiparty interactions.

The timed API facilitates implementation of real-time distributed protocols.

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 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.