Nested Monitors: Monitors as Expressions to Build Monitors

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.