How to Verify Your Python Conversations

Abstract

In large-scale distributed systems, each application is realised through inter- actions among distributed components. To guarantee safe communication (no deadlocks and communication mismatches) we need programming lan- guages and tools that structure, manage, and policy-check these interactions. Multiparty session types (MSPT), a typing discipline for structured inter- actions 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 primi- tives 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, fea- turing advanced Scribble primitives for verification of exception handling behaviours.