TY - GEN
T1 - SPY
T2 - 4th International Conference on Runtime Verification, RV 2013
AU - Neykova, Rumyana
AU - Yoshida, Nobuko
AU - Hu, Raymond
PY - 2013/11/18
Y1 - 2013/11/18
N2 - 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].
AB - 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].
UR - http://www.scopus.com/inward/record.url?scp=84887447109&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40787-1_25
DO - 10.1007/978-3-642-40787-1_25
M3 - Conference contribution
AN - SCOPUS:84887447109
SN - 9783642407864
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 358
EP - 363
BT - Runtime Verification - 4th International Conference, RV 2013, Proceedings
Y2 - 24 September 2013 through 27 September 2013
ER -