Runtime Verification of Real-Time Event Streams under Non-synchronized Arrival

@article {1320,
	title = {Runtime Verification of Real-Time Event Streams under Non-synchronized Arrival},
	journal = {Software Quality Journal},
	year = {2020},
	type = {Improving Software Quality through Formal Methods},
	abstract = {<p>We study the problem of online runtime verication of real-time<br>
	event streams. Our monitors can observe concurrent systems with a shared<br>
	clock, but where each component reports observations as signals that arrive to<br>
	the monitor at dierent speeds and with dierent and varying latencies. We<br>
	start from specications in a fragment of the TeSSLa specication language,<br>
	where streams (including inputs and nal verdicts) are not restricted to be<br>
	Booleans but can be data from richer domains, including integers and reals<br>
	with arithmetic operations and aggregations. Specications can be used both<br>
	for checking logical properties, and for computing statistics and general nu-<br>
	meric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for the specication language and a concurrent<br>
	implementation of the evaluation algorithm. The algorithm can tolerate and<br>
	exploit the asynchronous arrival of events without synchronizing the inputs.<br>
	Then, we introduce a theory of asynchronous transducers and show a formal<br>
	proof of the correctness such that every possible run of the monitor imple-<br>
	ments the semantics. Finally, we report an empirical evaluation of a highly<br>
	concurrent Erlang implementation of the monitoring algorithm.</p>
},
	author = {Martin Leucker and C{\'e}sar S{\'a}nchez and Torben Scheffel and Malte Schmitz and Alexander Schramm}
}