Runtime Verification for Timed Event Streams with Partial Information

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

*Corresponding author for this work


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.

Original languageEnglish
Title of host publicationRV 2019: Runtime Verification
EditorsBernd Finkbeiner, Leonardo Mariani
Number of pages19
Volume11757 LNCS
PublisherSpringer, Cham
Publication date01.10.2019
ISBN (Print)978-3-030-32078-2
ISBN (Electronic)978-3-030-32079-9
Publication statusPublished - 01.10.2019
Event19th International Conference on Runtime Verification - Porto, Portugal
Duration: 08.10.201911.10.2019
Conference number: 233219


Dive into the research topics of 'Runtime Verification for Timed Event Streams with Partial Information'. Together they form a unique fingerprint.

Cite this