elib
DLR-Header
DLR-Logo -> http://www.dlr.de
DLR Portal Home | Imprint | Privacy Policy | Contact | Deutsch
Fontsize: [-] Text [+]

Monitoring With Verified Guarantees

Dauer, Johann and Finkbeiner, Bernd and Schirmer, Sebastian (2021) Monitoring With Verified Guarantees. Springer. 21st International Conference on Runtime Verification, 11.-14. Okt. 2021, Virtual. doi: 10.1007/978-3-030-88494-9_4. ISBN 978-3-030-88494-9.

[img] PDF
534kB

Official URL: https://link.springer.com/chapter/10.1007/978-3-030-88494-9_4

Abstract

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.

Item URL in elib:https://elib.dlr.de/144534/
Document Type:Conference or Workshop Item (Speech)
Title:Monitoring With Verified Guarantees
Authors:
AuthorsInstitution or Email of AuthorsAuthor's ORCID iD
Dauer, JohannJohann.Dauer (at) dlr.dehttps://orcid.org/0000-0002-8287-2376
Finkbeiner, Berndfinkbeiner (at) cs.uni-sb.dehttps://orcid.org/0000-0002-4280-8441
Schirmer, Sebastiansebastian.schirmer (at) dlr.dehttps://orcid.org/0000-0002-4596-2479
Date:11 October 2021
Refereed publication:Yes
Open Access:Yes
Gold Open Access:No
In SCOPUS:No
In ISI Web of Science:No
DOI :10.1007/978-3-030-88494-9_4
Page Range:pp. 62-80
Publisher:Springer
Series Name:Lecture Notes in Computer Science (LNCS), Band 12974
ISBN:978-3-030-88494-9
Status:Published
Keywords:Formal methods, Cyber-physical systems, Runtime verification, Hoare logic
Event Title:21st International Conference on Runtime Verification
Event Location:Virtual
Event Type:international Conference
Event Dates:11.-14. Okt. 2021
HGF - Research field:Aeronautics, Space and Transport
HGF - Program:Aeronautics
HGF - Program Themes:Components and Systems
DLR - Research area:Aeronautics
DLR - Program:L CS - Components and Systems
DLR - Research theme (Project):L - Unmanned Aerial Systems
Location: Braunschweig
Institutes and Institutions:Institute of Flight Systems > Unmanned Aircraft
Deposited By: Schirmer, Sebastian
Deposited On:06 Dec 2021 21:45
Last Modified:15 Mar 2022 08:14

Repository Staff Only: item control page

Browse
Search
Help & Contact
Information
electronic library is running on EPrints 3.3.12
Copyright © 2008-2017 German Aerospace Center (DLR). All rights reserved.