Search papers, labs, and topics across Lattice.
This paper introduces RLola, an enhanced stream-based specification language designed for monitoring cyber-physical systems under measurement noise. By incorporating slack variables to symbolically represent noise and developing algorithms for both online and offline monitoring, RLola addresses the challenges of inaccurate sensor data while ensuring constant memory usage for real-time applications. The evaluation shows that RLola can effectively detect violations that traditional monitoring methods might overlook, thereby improving the reliability of safety assessments in dynamic environments.
RLola can detect safety violations in cyber-physical systems that traditional monitoring methods miss, even in the presence of 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 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. We present algorithms for both online and offline monitoring of RLola specifications. Since monitoring RLola specifications may require unbounded memory in general, we identify a rich fragment of RLola that can be automatically translated into monitors with guaranteed constant memory usage for online monitoring. An online RLola monitor observes a live system and provides real-time feedback on the current status of specified assertions. A satisfiability-modulo-theories-based offline algorithm analyzes complete system traces and determines whether a hypothetical ground-truth trace exists that satisfies all assertions at all time points. The offline algorithm can therefore detect violations that the online algorithm may miss. We implement these algorithms in the existing RTLola framework and evaluate their precision and running time based on a comprehensive example.
