Runtime Verification of Generalized Test Tables

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Alexander Weigl, Mattias Ulbrich, Shmuel S. Tyszberowicz und Jonas Klamroth
In:NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:12673
Jahr:2021
Seiten:358-374
Preprint/PDF:nfm2021.pdf
DOI:10.1007/978-3-030-76384-8_22
Links:

Abstract

Runtime verification allows validation of systems during their operation by monitoring crucial system properties. It is common to generate monitors from temporal specifications formulated in languages like MTL or LTL. However, writing formal specifications might be an obstacle for practitioners. In this paper we present an approach and a tool for generating software monitors for reactive systems from a set of Generalized Test Tables (gtts) – a table-based, user-friendly specification language specially designed for engineers. The tool is a valuable addition to the already existing static verifier for gtts since assumptions made in specifications can thus be validated at runtime. Moreover, it makes software and specifications amenable for formal validation that cannot be verified statically. Moreover, the approach is particularly well-suited for the specification of workflows as a collection of tables since it supports dynamic, trigger-based spawning of monitors. The tool produces monitor code in C++ for tables provided in an existing table definition format. We show the usefulness of our approach using characteristic examples.

BibTeX

@inproceedings{WeiglUlbrichEtAl2021,
  author    = {Alexander Weigl and
               Mattias Ulbrich and
               Shmuel S. Tyszberowicz and
               Jonas Klamroth},
  title     = {Runtime Verification of Generalized Test Tables},
  booktitle = {{NASA} Formal Methods - 13th International Symposium, {NFM} 2021,
               Virtual Event, May 24-28, 2021, Proceedings},
  editor    = {Aaron Dutle and
               {Mariano M.} Moscato and
               Laura Titolo and
               {C{\'{e}}sar A.} Mu{\~{n}}oz and
               Ivan Perez},
  series    = {Lecture Notes in Computer Science},
  volume    = {12673},
  pages     = {358--374},
  publisher = {Springer},
  year      = {2021},
  month     = may,
  doi       = {10.1007/978-3-030-76384-8\_22}
}