SPY: Local verification of global protocols

Rumyana Neykova, Nobuko Yoshida, Raymond Hu

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

25 Citations (Scopus)


This paper presents a toolchain for designing deadlock-free multiparty global protocols, and their run-time verification through automatically generated, distributed endpoint monitors. Building on the theory of multiparty session types, our toolchain implementation validates communication safety properties on the global protocol, but enforces them via independent monitoring of each endpoint process. Each monitor can be internally embedded in or externally deployed alongside the endpoint runtime, and detects the occurrence of illegal communication actions and message types that do not conform to the protocol. The global protocol specifications can be additionally elaborated to express finer-grained and higher-level requirements, such as logical assertions on message payloads and security policies, supported by third-party plugins. Our demonstration use case is the verification of choreographic communications in a large cyberinfrastructure for oceanography [10].

Original languageEnglish
Title of host publicationRuntime Verification - 4th International Conference, RV 2013, Proceedings
Number of pages6
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 'SPY: Local verification of global protocols'. Together they form a unique fingerprint.

Cite this