Runtime verification of real-time event streams under non-synchronized arrival

Abstract

We present a stream based runtime verification language designed for real-time signals and asynchronous behaviors. Our event streams are asynchronous because events can occur in event streams at different points in time. We present a novel specification language called TeSSLA for specifying properties of such systems. Our asynchronous streams, including the inputs and final verdicts, are not restricted to be Booleans but can be from richer data domains. Likewise, TeSSLA includes arithmetic operations and aggregations. In consequence, TeSSLA can be used for checking real-time properties but also for computing statistics and general numeric temporal 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 present a highly concurrent Erlang implementation of the monitoring algorithm and report on an empirical evaluation.