Nested Monitors: Monitors as Expressions to Build Monitors

Abstract

Stream runtime verification (SRV) is a formalism to express monitors as relations between typed input streams (observations) and typed output streams (data verdicts). In SRV, the actual data operations are separated from the temporal dependencies, therefore generalizing monitoring algorithms for temporal logics into the computation of richer verdicts. In this paper we study a new and powerful feature, which consists of lifting the execution of monitors to functions that can be used in defining expressions of enclosing specifications. At runtime, the outer monitor invokes the inner monitor passing a list of input events, called a slice. We present nested monitors for synchronous streams and for real-time event streams, allowing the elegant description of many specifications of interest, while still keeping the resources bounded. We formally describe nested monitors and slices, and illustrate the practical application in many real-life examples, including electrocardiogram analysis (QRS), quantitative Metric Temporal Logic and arbitrary robustness of Signal Temporal Logic specifications.