Runtime Verification for Timed Event Streams with Partial Information

Martin Leucker*, César Sánchez, Torben Scheffel, Malte Schmitz, Daniel Thoma

*Korrespondierende/r Autor/-in für diese Arbeit

Abstract

Runtime Verification (RV) studies how to analyze execution traces of a system under observation. Stream Runtime Verification (SRV) applies stream transformations to obtain information from observed traces. Incomplete traces with information missing in gaps pose a common challenge when applying RV and SRV techniques to real-world systems as RV approaches typically require the complete trace without missing parts. This paper presents a solution to perform SRV on incomplete traces based on abstraction. We use TeSSLa as specification language for non-synchronized timed event streams and define abstract event streams representing the set of all possible traces that could have occurred during gaps in the input trace. We show how to translate a TeSSLa specification to its abstract counterpart that can propagate gaps through the transformation of the input streams and thus generate sound outputs even if the input streams contain gaps and events with imprecise values. The solution has been implemented as a set of macros for the original TeSSLa and an empirical evaluation shows the feasibility of the approach.

OriginalspracheEnglisch
TitelRV 2019: Runtime Verification
Redakteure/-innenBernd Finkbeiner, Leonardo Mariani
Seitenumfang19
Band11757 LNCS
Herausgeber (Verlag)Springer, Cham
Erscheinungsdatum01.10.2019
Seiten273-291
ISBN (Print)978-3-030-32078-2
ISBN (elektronisch)978-3-030-32079-9
DOIs
PublikationsstatusVeröffentlicht - 01.10.2019
Veranstaltung19th International Conference on Runtime Verification - Porto, Portugal
Dauer: 08.10.201911.10.2019
Konferenznummer: 233219

Fingerprint

Untersuchen Sie die Forschungsthemen von „Runtime Verification for Timed Event Streams with Partial Information“. Zusammen bilden sie einen einzigartigen Fingerprint.

Zitieren