@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}
}
Runtime Verification of Generalized Test Tables
| Author(s): | Alexander Weigl, Mattias Ulbrich, Shmuel S. Tyszberowicz, and Jonas Klamroth |
|---|---|
| In: | NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings |
| Publisher: | Springer |
| Series: | Lecture Notes in Computer Science |
| Volume: | 12673 |
| Year: | 2021 |
| Pages: | 358-374 |
| Preprint/PDF: | nfm2021.pdf |
| DOI: | 10.1007/978-3-030-76384-8_22 |
| Links: | The final publication is available at Springer. |
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.