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, which we have 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 in order to constrain the times in which interactions 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. To demonstrate the practicality of the proposed framework, we express and verify four categories of widely used temporal patterns from use cases in literature. We analyse the performance of our implementation via benchmarking and show negligible overhead.

@article{NBY2017,
  author = {Rumyana Neykova and Laura Bocchi and Nobuko Yoshida},
  title = {{Timed Runtime Monitoring for Multiparty Conversations}},
  journal = {FAOC},
  pages = {1--34},
  publisher = {Springer},
  year = 2017
}

@article{NBY2017,
  author = {Rumyana Neykova and Laura Bocchi and Nobuko Yoshida},
  title = {{Timed Runtime Monitoring for Multiparty Conversations}},
  journal = {Formal Aspects of Computing},
  pages = {1--34},
  publisher = {Springer},
  doi = "10.1007/s00165-017-0420-8",
  year = 2017
}