Change search
ReferencesLink to record
Permanent link

Direct link
Runtime monitoring for concurrent systems
KTH. National Institute of Advanced Industrial Science and Technology (AIST), Japan.
Show others and affiliations
2016 (English)In: 16th International Conference on Runtime Verification, RV 2016, Springer, 2016, 386-403 p.Conference paper (Refereed)
Abstract [en]

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.
Keyword [en]
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
National Category
Computer Systems
URN: urn:nbn:se:kth:diva-195445DOI: 10.1007/978-3-319-46982-9_24ScopusID: 2-s2.0-84990210226ISBN: 9783319469812OAI: diva2:1050263
23 September 2016 through 30 September 2016

Funding Details: JP26280019, JSPS, Japan Society for the Promotion of Science

QC 20161128

Available from: 2016-11-28 Created: 2016-11-03 Last updated: 2016-11-28Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Artho, Cyrille
By organisation
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 8 hits
ReferencesLink to record
Permanent link

Direct link