Stream-Based Monitoring Under Measurement Noise

Stream-based monitoring is a runtime verification approach for cyber-physical systems that translates streams of input data, such as sensor readings, into streams of aggregate statistics and verdicts about the safety of the running system. It is usually assumed that the values on the input streams represent fully accurate measurements of the physical world. In reality, however, physical sensors are prone to measurement noise and errors. These errors are further amplified by the processing and aggregation steps within the monitor. This paper introduces RLola, a robust extension of the stream-based specification language Lola. RLola incorporates the concept of slack variables, which symbolically represent measurement noise while avoiding the aliasing problem of interval arithmetic. With RLola, standard sensor error models can be expressed directly in the specification. While the monitoring of RLola specifications may, in general, require an unbounded amount of memory, we identify a rich fragment of RLola that can automatically be translated into precise monitors with guaranteed constant-memory consumption.