Timed Runtime Monitoring for Multiparty Conversations
Rumyana Neykova, Laura Bocchi, Nobuko Yoshida
In [tMPST] we present a real-time extension of Multiparty Session Types to the verification and enforcement of time-related properties in Python. The prototype implementation is available at bottom of this page.
1. Context and Background
(Untimed) Multiparty Session Types (MPSTs) have been applied in an
existing framework for verification of choreographic sessions in Python
This framework is embedded into the OOI infrastructure using Scribble, a
practical incarnation of MPSTs, as a specification language for global
2. An Application of Timed Multiparty Session Types
In the OOI infrastructure time plays a crucial role. In most of the OOI
use-cases, service requests are augmented with deadlines and
services are scheduled to execute at certain time intervals to minimise
energy consumption. In
we have extended the MPSTs framework with time to accommodate these requirements.
In this section we discuss a practical application of the timed MPTSs presented in
We have extended Scribble with clocks and clock constraints;
(timed) global specifications are checked by the Scribble compiler for
feasibility and wait-freedom, and then projected by the
Scribble toolchain (as in Section 2 [tMPST]). The figure below shows
how we express the Global protocol for the WordCount example
Clocks constraints and reset predicates are enclosed by square brackets.
In [x@M:x=0,reset(x)] the constraint states that the next action of M, namely sending the task to W,
must be executed when the value of clock x of M is 0, and then the clock of M must be reset.
Timed Implementations: from Timed Processes to Python
We extend the Python conversation API with time for distributed runtime processes.
The figure below shows the Python program for process the master role.
Letter s denotes the session, while w and a are the queues of W and R, respectively.
The conversation API has two main primitives (we abstract on the session initialisation): send and receive.
For instance, send(a).task sends a message of type task to R, and the receive is dual.
Each participant is implemented as a virtual thread using a Python library for cooperative scheduling called "gevent".
We extended the API with the primitive s.delay which correspond to the delay operator of our calculus.
In order to handle time violations we have introduced the primitive s.timeout which raises an error if
the next instruction cannot be completed in the given time frame.
Running the Implementation
The implementation can be downloaded here.
The instructions for installing and running the prototype are in the included file readme.txt. If case of any problem while installing or running the application
please contact us.
Remark: In the prototype, time is expressed in seconds.
In order to speed up the demonstration, the delays l (latency) and w (sampling time) of the running example have not been set to the values in the paper (and in the OOI case study), but to smaller values. These values can be modified by editing the
timed local types in the zip file (see the file readme.txt included in the .zip for the location of the corresponding files).