Runtime Monitoring for Concurrent Systems
2016 (English)In: 16th International Conference on Runtime Verification, RV 2016, Springer, 2016, Vol. 10012, 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. Vol. 10012, 386-403 p.
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10012
CSP, Parametric monitoring, Process algebra, Runtime monitoring
IdentifiersURN: urn:nbn:se:kth:diva-199095DOI: 10.1007/978-3-319-46982-9_24ScopusID: 2-s2.0-84990210226ISBN: 9783319469812OAI: oai:DiVA.org:kth-199095DiVA: diva2:1062024
16th International Conference on Runtime Verification, RV 2016, Madrid, Spain, 23 September 2016 through 30 September 2016
QC 201701192017-01-042016-12-282017-01-19Bibliographically approved