Advertisement
Published in:
2014 | OriginalPaper | Chapter
Foundations of Boolean Stream Runtime Verification
Authors : Laura Bozzelli, César Sánchez
Published in: Runtime Verification
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.