Runtime monitoring for concurrent systems

Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, Mitsuharu Yamamoto

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationRuntime Verification - 16th International Conference, RV 2016, Proceedings
EditorsYliès Falcone, César Sánchez
PublisherSpringer Verlag
Number of pages18
ISBN (Print)9783319469812
Publication statusPublished - 2016
Externally publishedYes
Event16th International Conference on Runtime Verification, RV 2016 - Madrid, Spain
Duration: Sept 23 2016Sept 30 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10012 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference16th International Conference on Runtime Verification, RV 2016

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Runtime monitoring for concurrent systems'. Together they form a unique fingerprint.

Cite this