TY - GEN
T1 - Runtime monitoring for concurrent systems
AU - Yamagata, Yoriyuki
AU - Artho, Cyrille
AU - Hagiya, Masami
AU - Inoue, Jun
AU - Ma, Lei
AU - Tanabe, Yoshinori
AU - Yamamoto, Mitsuharu
N1 - Funding Information:
We are grateful to Giles Reger for helping to develop the QEA models, and to Eijiro Sumii for helping us to develop the proof of Theorem . Yoshinao Isobe influenced the early design of the language. This work was supported by JSPS KAKENHI Grant Number JP26280019. We would like to thank Editage ( www.editage.jp ) for English-language editing.
Publisher Copyright:
© Springer International Publishing AG 2016.
PY - 2016
Y1 - 2016
N2 - Most existing specification languages for runtime verification describe the properties of the entire system in a top-down manner, and lack constructs to describe concurrency in the specification directly. CSPE is a runtime-monitoring framework based on Hoare’s Communicating Sequential Processes (CSP) that captures concurrency in the specification directly. In this paper, we define the syntax of CSPE and its formal semantics. In comparison to quantified event automata (QEA), as an example, CSPE describes a specification for a concurrent system in a bottom-up manner, whereas QEA lends itself to a top-down manner. We also present an implementation of CSPE, which supports full CSPE without optimization. When comparing its performance to that of QEA, our implementation of CSPE requires slightly more than twice the time required by QEA; we consider this overhead to be acceptable. Finally, we introduce a tool named stracematch, which is developed using CSPE. It monitors system calls in (Mac) OS X and verifies the usage of file descriptors by a monitored process.
AB - Most existing specification languages for runtime verification describe the properties of the entire system in a top-down manner, and lack constructs to describe concurrency in the specification directly. CSPE is a runtime-monitoring framework based on Hoare’s Communicating Sequential Processes (CSP) that captures concurrency in the specification directly. In this paper, we define the syntax of CSPE and its formal semantics. In comparison to quantified event automata (QEA), as an example, CSPE describes a specification for a concurrent system in a bottom-up manner, whereas QEA lends itself to a top-down manner. We also present an implementation of CSPE, which supports full CSPE without optimization. When comparing its performance to that of QEA, our implementation of CSPE requires slightly more than twice the time required by QEA; we consider this overhead to be acceptable. Finally, we introduce a tool named stracematch, which is developed using CSPE. It monitors system calls in (Mac) OS X and verifies the usage of file descriptors by a monitored process.
UR - http://www.scopus.com/inward/record.url?scp=84990210226&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84990210226&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-46982-9_24
DO - 10.1007/978-3-319-46982-9_24
M3 - Conference contribution
AN - SCOPUS:84990210226
SN - 9783319469812
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 386
EP - 403
BT - Runtime Verification - 16th International Conference, RV 2016, Proceedings
A2 - Falcone, Yliès
A2 - Sánchez, César
PB - Springer Verlag
T2 - 16th International Conference on Runtime Verification, RV 2016
Y2 - 23 September 2016 through 30 September 2016
ER -