CISPA
Browse
cispa_all_3684.pdf (521.69 kB)

Monitoring with Verified Guarantees

Download (521.69 kB)
conference contribution
posted on 2023-11-29, 18:19 authored by 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 guarantees of the correctness of the monitor. In this paper, we present a verification extension to the Lola monitoring language that integrates 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 led to the discovery of safety-critical errors in the specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns.

History

Preferred Citation

Johann Dauer, Bernd Finkbeiner and Sebastian Schirmer. Monitoring with Verified Guarantees. In: International Conference on Runtime Verification (RV). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Conference on Runtime Verification (RV)

Legacy Posted Date

2022-05-10

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3684, title = "Monitoring with Verified Guarantees", author = "Dauer, Johann C. and Finkbeiner, Bernd and Schirmer, Sebastian", booktitle="{International Conference on Runtime Verification (RV)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC