Runtime monitoring for concurrent systems
2016 (English)In: 16th International Conference on Runtime Verification, RV 2016, Springer, 2016, 386-403 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
Springer, 2016. 386-403 p.
CSP, Parametric monitoring, Process algebra, Runtime monitoring, Formal methods, Monitoring, Semantics, Specification languages, Specifications, Bottom-up manner, Communicating sequential process, Concurrent systems, Formal Semantics, Process algebras, Run-time verification, Top-down manner, Computer operating procedures
IdentifiersURN: urn:nbn:se:kth:diva-195445DOI: 10.1007/978-3-319-46982-9_24ScopusID: 2-s2.0-84990210226ISBN: 9783319469812OAI: oai:DiVA.org:kth-195445DiVA: diva2:1050263
23 September 2016 through 30 September 2016
Funding Details: JP26280019, JSPS, Japan Society for the Promotion of Science
QC 201611282016-11-282016-11-032016-11-28Bibliographically approved