TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams
| Title | TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams |
| Publication Type | Conference Paper |
| Year of Publication | 2018 |
| Authors | Leucker, M, Sánchez, C, Scheffel, T, Schmitz, M, Schramm, A |
| Conference Name | ACM Symposium on Applied Computing (SAC) |
| Date Published | 04/2018 |
| Publisher | ACM |
| Conference Location | France |
| Abstract | We present TeSSLa, a specification language based on stream runtime verification, designed for monitoring a specific class of realtime signals. Our monitors can observe concurrent systems with a shared clock, but where each component reports observations as signals that arrive to the monitor at different speeds and with different and varying latencies. The signals and streams that TeSSLa supports (including inputs and final verdicts) are not restricted to be Booleans but can be data from richer domains, including integers and reals with arithmetic operations and aggregations. Consequently, TeSSLa can be used both for checking logical properties, and for computing statistics and general numeric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for TeSSLa specifications and show a formal proof of the correctness of concurrent implementations of the evaluation algorithm. Finally, we report an empirical evaluation of a highly concurrent Erlang implementation of the monitoring algorithm. |
@inproceedings {1295,
title = {TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams},
booktitle = {ACM Symposium on Applied Computing (SAC)},
year = {2018},
month = {04/2018},
publisher = {ACM},
organization = {ACM},
address = {France},
abstract = {<p>We present TeSSLa, a specification language based on stream runtime verification, designed for monitoring a specific class of realtime signals. Our monitors can observe concurrent systems with a shared clock, but where each component reports observations as signals that arrive to the monitor at different speeds and with different and varying latencies. The signals and streams that TeSSLa supports (including inputs and final verdicts) are not restricted to be Booleans but can be data from richer domains, including integers and reals with arithmetic operations and aggregations. Consequently, TeSSLa can be used both for checking logical properties, and for computing statistics and general numeric temporal metrics (and properties on these richer metrics). We present an online evaluation algorithm for TeSSLa specifications and show a formal proof of the correctness of concurrent implementations of the evaluation algorithm. Finally, we report an empirical evaluation of a highly 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}
}