Runtime Verification For Timed Event Streams With Partial Information

@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}
}