MobilityReadingGroup

Timed Runtime Monitoring for Multiparty Conversations

Rumyana NEYKOVA , Laura BOCCHI , Nobuko YOSHIDA

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.

@inproceedings{NBY2014,
  author = {Rumyana Neykova and Laura Bocchi and Nobuko Yoshida},
  title = {{Timed Runtime Monitoring for Multiparty Conversations}},
  booktitle = {3rd International Workshop on Behavioural Types},
  volume = {162},
  pages = {19--26},
  publisher = {EPTCS},
  year = 2014
}

@inproceedings{NBY2014,
  author = {Rumyana Neykova and Laura Bocchi and Nobuko Yoshida},
  title = {{Timed Runtime Monitoring for Multiparty Conversations}},
  booktitle = {3rd International Workshop on Behavioural Types},
  volume = {162},
  pages = {19--26},
  publisher = {EPTCS},
  doi = "10.4204/EPTCS.162.3",
  year = 2014
}