Stream runtime verification of real-time event streams with the Striver language

Abstract

In this paper we study the problem of runtime verification of real-time event streams, in particular we propose a language to describe monitors for real-time event streams that can manipulate data from rich domains. We propose a solution based on stream runtime verification (SRV), where monitors are specified by describing how output streams of data are computed from input streams of data. SRV enables a clean separation between the temporal dependencies among incoming events, and the concrete operations that are performed during the monitoring. Most SRV specification languages assume that all streams share a global synchronous clock, and divide time in discrete instants. At each instant every input has a reading and for every instant the monitor computes an output. In this paper we generalize the time assumption to cover real-time event streams, but keep the explicit time offsets present in some synchronous SRV languages like Lola. The language we introduce, called Striver, shares with SRV the simplicity and economy of operators, and the separation between the reasoning about time and the computation of data values. The version of Striver in this paper allows expressing future and past dependencies. Striver is a general language that allows expressing for certain time domains other real-time monitoring languages, like TeSSLa, and temporal logics, like STL. We show in this paper translations from other formalisms for (piecewise-constant) real-time signals and timed event streams. Finally, we report an empirical evaluation of an implementation of Striver.