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

Abstract

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.