Dauer, Johann und Finkbeiner, Bernd und Schirmer, Sebastian (2021) Monitoring With Verified Guarantees. In: 21st International Conference on Runtime Verification, RV 2021, Seiten 62-80. Springer. 21st International Conference on Runtime Verification, 2021-10-11 - 2021-10-14, Virtual. doi: 10.1007/978-3-030-88494-9_4. ISBN 978-303088493-2. ISSN 0302-9743.
![]() |
PDF
534kB |
Offizielle URL: https://link.springer.com/chapter/10.1007/978-3-030-88494-9_4
Kurzfassung
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 lead 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.
elib-URL des Eintrags: | https://elib.dlr.de/144534/ | ||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Dokumentart: | Konferenzbeitrag (Vortrag) | ||||||||||||||||
Titel: | Monitoring With Verified Guarantees | ||||||||||||||||
Autoren: |
| ||||||||||||||||
Datum: | 11 Oktober 2021 | ||||||||||||||||
Erschienen in: | 21st International Conference on Runtime Verification, RV 2021 | ||||||||||||||||
Referierte Publikation: | Ja | ||||||||||||||||
Open Access: | Ja | ||||||||||||||||
Gold Open Access: | Nein | ||||||||||||||||
In SCOPUS: | Ja | ||||||||||||||||
In ISI Web of Science: | Ja | ||||||||||||||||
DOI: | 10.1007/978-3-030-88494-9_4 | ||||||||||||||||
Seitenbereich: | Seiten 62-80 | ||||||||||||||||
Verlag: | Springer | ||||||||||||||||
Name der Reihe: | Lecture Notes in Computer Science (LNCS), Band 12974 | ||||||||||||||||
ISSN: | 0302-9743 | ||||||||||||||||
ISBN: | 978-303088493-2 | ||||||||||||||||
Status: | veröffentlicht | ||||||||||||||||
Stichwörter: | Formal methods, Cyber-physical systems, Runtime verification, Hoare logic | ||||||||||||||||
Veranstaltungstitel: | 21st International Conference on Runtime Verification | ||||||||||||||||
Veranstaltungsort: | Virtual | ||||||||||||||||
Veranstaltungsart: | internationale Konferenz | ||||||||||||||||
Veranstaltungsbeginn: | 11 Oktober 2021 | ||||||||||||||||
Veranstaltungsende: | 14 Oktober 2021 | ||||||||||||||||
HGF - Forschungsbereich: | Luftfahrt, Raumfahrt und Verkehr | ||||||||||||||||
HGF - Programm: | Luftfahrt | ||||||||||||||||
HGF - Programmthema: | Komponenten und Systeme | ||||||||||||||||
DLR - Schwerpunkt: | Luftfahrt | ||||||||||||||||
DLR - Forschungsgebiet: | L CS - Komponenten und Systeme | ||||||||||||||||
DLR - Teilgebiet (Projekt, Vorhaben): | L - Unbemannte Flugsysteme | ||||||||||||||||
Standort: | Braunschweig | ||||||||||||||||
Institute & Einrichtungen: | Institut für Flugsystemtechnik > Unbemannte Luftfahrzeuge | ||||||||||||||||
Hinterlegt von: | Schirmer, Sebastian | ||||||||||||||||
Hinterlegt am: | 06 Dez 2021 21:45 | ||||||||||||||||
Letzte Änderung: | 24 Apr 2024 20:43 |
Nur für Mitarbeiter des Archivs: Kontrollseite des Eintrags