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

5 Citations (Scopus)

Abstract

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
Pages386-403
Number of pages18
ISBN (Print)9783319469812
DOIs
Publication statusPublished - Jan 1 2016
Externally publishedYes
Event16th International Conference on Runtime Verification, RV 2016 - Madrid, Spain
Duration: Sep 23 2016Sep 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

Conference

Conference16th International Conference on Runtime Verification, RV 2016
CountrySpain
CityMadrid
Period9/23/169/30/16

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Yamagata, Y., Artho, C., Hagiya, M., Inoue, J., Ma, L., Tanabe, Y., & Yamamoto, M. (2016). Runtime monitoring for concurrent systems. In Y. Falcone, & C. Sánchez (Eds.), Runtime Verification - 16th International Conference, RV 2016, Proceedings (pp. 386-403). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10012 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-46982-9_24