CISPA
Browse

Monitoring with verified guarantees

Download (3.53 MB)
journal contribution
posted on 2024-04-04, 06:56 authored by Jan BaumeisterJan Baumeister, Johann C Dauer, Bernd FinkbeinerBernd Finkbeiner, Sebastian Schirmer
Runtime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiating emergency protocols, as proposed in a recent aviation standard, then the safety of the entire system critically depends on the correctness of the monitor. In this paper, we present a verification extension to the LOLA monitoring language that extends the efficient specification of the monitor with Hoare-style annotations that guarantee the correctness of the monitor specification. We add two new operators, assume and assert, which specify assumptions of the monitor and expectations on its output, respectively. The validity of the annotations is established by an integrated SMT solver. We report on experience in applying the approach to specifications from the avionics domain, where the annotation with assumptions and assertions has lead to the discovery of safety-critical errors in specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns. We also report how verified specifications can be monitored efficiently at runtime.

History

Primary Research Area

  • Reliable Security Guarantees

Journal

International Journal on Software Tools for Technology Transfer

Volume

25

Page Range

593-616

Publisher

Springer Verlag

Open Access Type

  • Hybrid

Sub Type

  • Article

BibTeX

@article{Baumeister:Dauer:Finkbeiner:Schirmer:2023, title = "Monitoring with verified guarantees", author = "Baumeister, Jan" AND "Dauer, Johann C" AND "Finkbeiner, Bernd" AND "Schirmer, Sebastian", year = 2023, month = 8, journal = "International Journal on Software Tools for Technology Transfer", number = "4", pages = "593--616", publisher = "Springer Verlag", issn = "0945-8115", doi = "10.1007/s10009-023-00712-3" }