MobilityReadingGroup

How to Verify Your Python Conversations

Rumyana NEYKOVA, Nobuko YOSHIDA

In large-scale distributed systems, each application is realised through interactions among distributed components. To guarantee safe communication (no deadlocks and communication mismatches) we need programming languages and tools that structure, manage, and policy-check these interactions. Multiparty session types (MSPT), a typing discipline for structured interactions between communicating processes, offers a promising approach. To date, however, session types applications have been limited to static verification, which is not always feasible and is often restrictive in terms of programming API and specifying policies. This chapter investigates the design and implementation of a runtime verification framework, ensuring conformance between programs and specifications. Specifications are written in Scribble, a protocol description language formally founded on MPST. The central idea of the approach is a runtime monitor, which takes a form of a communicating finite state machine, automatically generated from Scribble specifications, and a communication runtime stipulating a message format. We demonstrate Scribble-based runtime verification in manifold ways. First, we present a Python library, facilitated with session primitives and verification runtime. Second, we show examples from a large cyber-infrastructure project for oceanography, which uses the library as a communication medium. Third, we examine communication patterns, featuring advanced Scribble primitives for verification of exception handling behaviours.

@article{NY2017,
  author = {Rumyana Neykova and Nobuko Yoshida},
  title = {{How to Verify Your Python Conversations}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {77--98},
  publisher = {River Publishers},
  year = 2017
}

@article{NY2017,
  author = {Rumyana Neykova and Nobuko Yoshida},
  title = {{How to Verify Your Python Conversations}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {77--98},
  publisher = {River Publishers},
  doi = "10.13052/rp-9788793519817",
  year = 2017
}