Foundations of Boolean Stream Runtime Verification (Extended Version)
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.
In Proc. of the 5th Int'l Conf. on Runtime Verification (RV'14), vol 8734 of LNCS, pp 64-79, Springer, 2014. ISBN 978-3-319-11163-6. Extended version.