SPY: local verification of global protocols. 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 .
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Bocchi, Laura; Chen, Tzu-Chun; Demangeon, Romain; Honda, Kohei; Yoshida, Nobuko: Monitoring networks through multiparty session types (2017)
- Neykova, Rumyana; Bocchi, Laura; Yoshida, Nobuko: Timed runtime monitoring for multiparty conversations (2017)
- Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Padovani, Luca; Yoshida, Nobuko: A gentle introduction to multiparty asynchronous session types (2015)
- Lanese, Ivan; Montesi, Fabrizio; Zavattaro, Gianluigi: The evolution of Jolie. From orchestrations to adaptable choreographies (2015)
- Yoshida, Nobuko; Hu, Raymond; Neykova, Rumyana; Ng, Nicholas: The Scribble protocol language (2014) ioport
- Neykova, Rumyana; Yoshida, Nobuko; Hu, Raymond: SPY: Local verification of global protocols (2013) ioport