Runtime Veri cation of Real-Time Event Streams under Non-synchronized Arrival

TitleRuntime Veri cation of Real-Time Event Streams under Non-synchronized Arrival
Publication TypeJournal Article
Year of Publication2019
AuthorsLeucker, M, Sánchez, C, Scheffel, T, Schmitz, M, Schramm, A
JournalSoftware Quality Journal
Type of ArticleImproving Software Quality through Formal Methods
Abstract

We study the problem of online runtime veri cation of real-time
event streams. Our monitors can observe concurrent systems with a shared
clock, but where each component reports observations as signals that arrive to
the monitor at di erent speeds and with di erent and varying latencies. We
start from speci cations in a fragment of the TeSSLa speci cation language,
where streams (including inputs and nal verdicts) are not restricted to be
Booleans but can be data from richer domains, including integers and reals
with arithmetic operations and aggregations. Speci cations can be used both
for checking logical properties, and for computing statistics and general nu-
meric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for the speci cation language and a concurrent
implementation of the evaluation algorithm. The algorithm can tolerate and
exploit the asynchronous arrival of events without synchronizing the inputs.
Then, we introduce a theory of asynchronous transducers and show a formal
proof of the correctness such that every possible run of the monitor imple-
ments the semantics. Finally, we report an empirical evaluation of a highly
concurrent Erlang implementation of the monitoring algorithm.

Bibtex: 
@article {1320,
	title = {Runtime Verication of Real-Time Event Streams under Non-synchronized Arrival},
	journal = {Software Quality Journal},
	year = {2019},
	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}
}
PDF: