Practical interruptible conversations: Distributed dynamic verification with session types and Python

Raymond Hu, Rumyana Neykova, Nobuko Yoshida, Romain Demangeon, Kohei Honda

Research output: Chapter in Book/Report/Conference proceedingConference contribution

30 Citations (Scopus)


The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations [33,28] on Scribble, a choreography description language based on multiparty session types, this paper proposes a dynamic verification framework for structured interruptible conversation programming. We first present our extension of Scribble to support the specification of asynchronously interruptible conversations. We then implement a concise API for conversation programming with interrupts in Python that enables session types properties to be dynamically verified for distributed processes. Our framework ensures the global safety of a system in the presence of asynchronous interrupts through independent runtime monitoring of each endpoint, checking the conformance of the local execution trace to the specified protocol. The usability of our framework for describing and verifying choreographic communications has been tested by integration into the large scientific cyberinfrastructure developed by the Ocean Observatories Initiative. Asynchronous interrupts have proven expressive enough to represent and verify their main classes of communication patterns, including asynchronous streaming and various timeout-based protocols, without requiring additional synchronisation mechanisms. Benchmarks show conversation programming and monitoring can be realised with little overhead.

Original languageEnglish
Title of host publicationRuntime Verification - 4th International Conference, RV 2013, Proceedings
Number of pages19
Publication statusPublished - 18 Nov 2013
Externally publishedYes
Event4th International Conference on Runtime Verification, RV 2013 - Rennes, France
Duration: 24 Sept 201327 Sept 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8174 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference4th International Conference on Runtime Verification, RV 2013


Dive into the research topics of 'Practical interruptible conversations: Distributed dynamic verification with session types and Python'. Together they form a unique fingerprint.

Cite this