Foundations of Boolean Stream Runtime Verification

Abstract

Stream runtime verification (\SRV), pioneered by the tool LOLA, is a declarative approach to specify synchronous monitors. In \SRV, monitors are described by specifying dependencies between output streams of values and input streams of values. The declarative nature of \SRV enables a separation between (1) the evaluation algorithms, and (2) the monitor storage and its individual updates. This separation allows \SRV to be lifted from conventional failure monitors into richer domains to collect statistics of traces. Moreover, \SRV allows to easily identify specifications that can be efficiently monitored online, and to generate efficient schedules for offline monitors. In spite of these attractive features, many important theoretical problems about \SRV are still open. In this paper, we address complexity, expressiveness, succinctness, and closure issues for the subclass of Boolean \SRV (\BSRV) specifications. Additionally, we show that for this subclass, offline monitoring can be performed with only two passes (one forward and one backward) over the input trace in spite of the alternation of past and future references in the \BSRV specification.