# Runtime Verification For Timed Event Streams With Partial Information

 Title Runtime Verification For Timed Event Streams With Partial Information Publication Type Conference Paper Year of Publication 2019 Authors Leucker, M, Sánchez, C, Scheffel, T, Schmitz, M, Thoma, D Conference Name Runtime Verification (RV) Publisher Springer Conference Location Portugal 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.
Bibtex:
@inproceedings {1319,
title = {Runtime Verification For Timed Event Streams With Partial Information},
booktitle = {Runtime Verification (RV)},
year = {2019},
publisher = {Springer},
organization = {Springer},
abstract = {<p>Runtime Verification (RV) studies how to analyze execution<br>
traces of a system under observation. Stream Runtime Verification (SRV)<br>
applies stream transformations to obtain information from observed<br>
traces. Incomplete traces with information missing in gaps pose a common<br>
challenge when applying RV and SRV techniques to real-world systems<br>
as RV approaches typically require the complete trace without missing<br>
parts. This paper presents a solution to perform SRV on incomplete<br>
traces based on abstraction. We use TeSSLa as specification language<br>
for non-synchronized timed event streams and define abstract event<br>
streams representing the set of all possible traces that could have occurred<br>
during gaps in the input trace. We show how to translate a TeSSLa<br>
specification to its abstract counterpart that can propagate gaps through<br>
the transformation of the input streams and thus generate sound outputs<br>
even if the input streams contain gaps and events with imprecise values.<br>
The solution has been implemented as a set of macros for the original<br>
TeSSLa and an empirical evaluation shows the feasibility of the approach.</p>
},
author = {Martin Leucker and C{\'e}sar S{\'a}nchez and Torben Scheffel and Malte Schmitz and Daniel Thoma}
}
PDF: