Offline and online energy-efficient monitoring of scattered uncertain logs using a bounding model

TL;DR

This work addresses safety monitoring for distributed cyber-physical systems when logs are incomplete, uncertain in both state and timestamp, and the true dynamics are unknown. It introduces an over-approximate bounding model using uncertain linear dynamical systems and leverages reachability-based offline and online monitoring to detect potential safety violations with formal guarantees on discrete timestamps. Offline monitoring extrapolates from known samples while online monitoring schedules the next sample to minimize energy and bandwidth, achieving substantial reductions in sampling while preserving safety guarantees. The approach is implemented in MoULDySGHOSH2023102976 and validated on three benchmarks (anesthesia, adaptive cruise control, and aircraft orbiting), demonstrating robust handling of log and timestamp uncertainties and offering practical energy-efficient monitoring for real-world CPS deployments.

Abstract

Monitoring the correctness of distributed cyber-physical systems is essential. Detecting possible safety violations can be hard when some samples are uncertain or missing. We monitor here black-box cyber-physical system, with logs being uncertain both in the state and timestamp dimensions: that is, not only the logged value is known with some uncertainty, but the time at which the log was made is uncertain too. In addition, we make use of an over-approximated yet expressive model, given by a non-linear extension of dynamical systems. Given an offline log, our approach is able to monitor the log against safety specifications with a limited number of false alarms. As a second contribution, we show that our approach can be used online to minimize the number of sample triggers, with the aim at energetic efficiency. We apply our approach to three benchmarks, an anesthesia model, an adaptive cruise controller and an aircraft orbiting system.

Figures (11)

• Figure 1: Monitoring at discrete time steps
• Figure 2: (\ref{['fig:offline_monitoring']}): Offline Monitoring. Black: Two consecutive samples, $k$ and $k+1$, at time steps $t$ and $t+5$ respectively. Blue: The over-approximate reachable set computed from sample $k$ using overReach(.). (\ref{['fig:online_monitoring']}): Online Monitoring. Blue: Over-approximate reachable set computed, at each step, using overReach(.).
• Figure 3: Offline Monitoring (Anesthesia). We plot the change in concentration level of $c_p$ with time. The volume of the samples increases from left to right, and the probability of logging increases from bottom to top. The blue regions are the reachable sets showing the over-approximate reachable sets as computed by the offline monitoring, the black regions are the samples from the log given to the offline monitoring algorithm, and the red dotted line represents safe distance level. Note that although \ref{['fig:anesthesia_fig1', 'fig:anesthesia_fig4']} reachable sets' seem to intersect with the red line (unsafe set), the refinement module infers them to be unreachable, therefore concluding the system behavior as safe---unlike \ref{['fig:anesthesia_fig2']}.
• Figure 4: Online Monitoring (Anesthesia). We plot the change in concentration level of $c_p$ with time. The blue regions are the reachable sets showing the over-approximate reachable sets as computed by the online monitoring, the black regions are the samples generated when the logging system was triggered by the online monitoring algorithm, and the red dotted line represents safe concentration levels. Online monitoring (\ref{['fig:anesthesia_online']}): We apply our online monitoring to the anesthesia model. Comparison (\ref{['fig:anesthesia_comp']}): We compare our online and offline algorithms. The green regions are the reachable sets showing the over-approximate reachable sets between two consecutive samples from the offline logs, the magenta regions are the offline logs, given as an input to the offline monitoring algorithm, generated by the logging system, and the red dotted line represents safe concentration levels. The blue regions are the reachable sets showing the over-approximate reachable sets as computed by the online monitoring, the black regions are the samples generated when the logging system was triggered by the online monitoring algorithm, and the red dotted line represents safe concentration levels.
• Figure 5: Offline Monitoring (ACC). We plot the change in distance $h$ between the vehicles with time. The volume of the samples increases from left to right, and the probability of logging increases from bottom to top.

Theorems & Definitions (13)

• Example 3.1: ghoshrobustreachset
• Definition 3.2: Uncertain linear dynamical systems (ghoshrobustreachset)
• Definition 3.3: Reachable set of an uncertain linear dynamical systems ( ghoshrobustreachset)
• Definition 3.4: Uncertain log
• Definition 3.5: Fixed timestamp uncertain log
• Theorem 4.1: soundness at discrete time steps for a fixed timestamp uncertain log
• proof
• Theorem 4.2: soundness at discrete time steps for an uncertain log
• proof
• Theorem 4.3: correctness at discrete time steps