TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams

Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Alexander Schramm


We present TeSSLa, a specification language based on stream run-time verification, designed for monitoring a specific class of real-time 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.

Original languageEnglish
Title of host publicationSAC '18 Proceedings of the 33rd Annual ACM Symposium on Applied Computing
Number of pages9
Publication date09.04.2018
ISBN (Print)978-145035191-1
Publication statusPublished - 09.04.2018
Event33rd Annual ACM Symposium on Applied Computing
- Pau, France
Duration: 09.04.201813.04.2018
Conference number: 137816


Dive into the research topics of 'TeSSLa: Runtime Verification of Non-synchronized Real-Time Streams'. Together they form a unique fingerprint.

Cite this