Runtime Verification For Timed Event Streams With Partial Information

TitleRuntime Verification For Timed Event Streams With Partial Information
Publication TypeConference Paper
Year of Publication2019
AuthorsLeucker, M, Sánchez, C, Scheffel, T, Schmitz, M, Thoma, D
Conference NameRuntime Verification (RV)
PublisherSpringer
Conference LocationPortugal
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},
	address = {Portugal},
	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: