Online Signal Monitoring With Bounded Lag

An essential approach for guaranteeing the safety of a cyber-physical system is to monitor its execution in real time. The execution trace of such a system typically consists of one or more signals, and a key computational task for safety monitoring is the online processing of these signals in order to identify events that need to be acted upon in a timely manner. There are several existing proposals for the specification of signal monitors: temporal logics, reactive languages, and dataflow formalisms. A shared feature of most of these proposals is that they describe online signal transformations that are causal. The causality requirement enables a real-time implementation, where the input and output signals are perfectly synchronized. We propose a new specification formalism for signal monitors that relaxes the causality restriction and allows the output to depend on a bounded amount of future input. It follows that an online implementation of such a monitor must have a certain amount of lag in the computation. We introduce a formal framework for signal transformations that allow bounded lag (the output has fallen behind the input) and bounded lead (the output is running ahead of the input), and we propose a type discipline for classifying these transformations according to their lead/lag. We show that this typed framework provides a modular approach for succinctly specifying: 1) monitors for temporal properties that involve both past and bounded-future connectives and 2) complex signal processing computations, such as those arising in the monitoring of physiological signals in medical devices. We have implemented the proposed specification formalism and we have compared it against state-of-the-art tools for the online monitoring of temporal properties: MonPoly, StreamLAB, Aerial, and Reelay.