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, Vol. 10012, 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. Vol. 10012, 386-403 p.
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10012
Keyword [en]
CSP, Parametric monitoring, Process algebra, Runtime monitoring
National Category
Computer Science
URN: urn:nbn:se:kth:diva-199095DOI: 10.1007/978-3-319-46982-9_24ScopusID: 2-s2.0-84990210226ISBN: 9783319469812OAI: diva2:1062024
16th International Conference on Runtime Verification, RV 2016, Madrid, Spain, 23 September 2016 through 30 September 2016

QC 20170119

Available from: 2017-01-04 Created: 2016-12-28 Last updated: 2017-01-19Bibliographically approved

Open Access in DiVA

fulltext(443 kB)0 downloads
File information
File name FULLTEXT01.pdfFile size 443 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Artho, Cyrille
By organisation
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

ReferencesLink to record
Permanent link

Direct link