Runtime Verification

As learning-enabled Cyber-Physical Systems (CPSs) are increasingly used in safety-critical settings, there is a growing need to ensure their safety. For example, to tackle the problem of rate-adaptive pacemakers which correct Sinus Node Dysfunction, a Reinforcement Learning (RL) approach may be used to mimic the natural pacing rhythm of the heart. However, this is currently not done and there are no known approaches to ensure the safety of combining RL with conventional pacing algorithms. While there is growing interest on ensuring the safety of AI-enabled CPS, the issue of safe RL for CPS, using light-weight formal methods, has drawn scant attention.

Therefore, we present an approach which combines Runtime Enforcement with RL. To guarantee safety throughout the RL agent’s learning and execution stages, an enforcer is constructed from a set of safety policies expressed using a variant of timed automata. The RL agent’s outputs are observed by the enforcer, which ensures that only safe actions are delivered to the environment by correcting the outputs which would violate the safety policies. In order to evaluate the proposed approach, we have implemented a rate-adaptive pacemaker which learns the natural pacing rhythm through an RL agent, allowing it to pace appropriately during disease. This model is executed in closed-loop with a real-time heart model where various diseases can be exhibited in order to test its efficacy. Furthermore, we illustrate the benefits of this system by contrasting it with traditional pacing techniques and RL without the use of an enforcer.

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.

When monitoring a cyber-physical system (CPS) from a remote server, keeping the monitored data secret is crucial, particularly when they contain sensitive information, e. g., biological or location data. Recently, Banno et al. (CAV’22) proposed a protocol for online LTL monitoring that keeps data concealed from the server using Fully Homomorphic Encryption (FHE). We build on this protocol to allow arithmetic operations over encrypted values, e. g., to compute a safety measurement combining distance, velocity, and so forth. Overall, our protocol enables oblivious online monitoring of discrete-time real-valued signals against signal temporal logic (STL) formulas. Our protocol combines two FHE schemes, CKKS and TFHE, leveraging their respective strengths. We employ CKKS to evaluate arithmetic predicates in STL formulas while utilizing TFHE to process them using a DFA derived from the STL formula. We conducted case studies on monitoring blood glucose levels and vehicles’ behavior against the Responsibility-Sensitive Safety (RSS) rules. Our results suggest the practical relevance of our protocol.

Safety-critical autonomous systems often operate in highly uncertain environments. These environments consist of many agents, some of which are being designed, and some represent the uncertain aspects of the environment. Testing autonomous systems requires generating diverse scenarios. However, the space of scenarios is very large, and many scenarios do not represent edge cases of the system. We want to develop a framework for automatically generating interesting scenarios. We propose to describe scenarios using a formal language. We show how we can extract interesting scenarios using scenario specifications from sampling-based approaches for scenario generation. We also introduce another technique for edge-case scenario generation using the gradient computation over STL. We demonstrate the capability of our framework in scenario generation in two case studies of autonomous systems involving the autonomous driving domain and the safety of human-robot systems in an industrial manufacturing context.

Optimization-based falsification is an automatic test generation method for evaluating the safety of Cyber-Physical Systems (CPS) against formal requirements. In this work, we focus on temporal logic requirements and, more specifically on Parametric Signal Temporal Logic (pSTL). pSTL generalizes STL allowing to express the quantifiers of the logical operators as variables. This extends the falsification from searching for the inputs that violate the requirement to the inputs and the formula parametrizations that result into unsafe behaviors. The state-of-the-art Part-X, a recent algorithm for falsification, offers probabilistic falsification level sets and confidence-bounded results on inputs but is not tailored for pSTL. Our approach, HyperPart-X, builds on Part-X and solves the problem while also providing probabilistic guarantees on the estimated level set by adaptively branching the parameter space and intelligently sampling from both the parameter and input spaces in a coordinated and hierarchical approach. HyperPart-X is compared on synthetic functions and CPS benchmarks against uniform random and Part-X . Empirical results demonstrate that HyperPart-X returns level set estimates and guarantees, where Part-X fails to find a solution. Results also show that it can achieve the level set with the same associated confidence level as uniform random sampling using orders of magnitude less samples.

State-of-the-art RV frameworks that implement runtime monitors in hardware synthesize monitoring circuits from formal specifications of properties. Such frameworks resynthesize or reconfigure monitoring circuits if the input properties change post-deployment. This is typically handled using reconfigurable fabrics such as FPGAs. Runtime monitors implemented on FPGAs have two disadvantages as compared to a fixed implementation (ASIC): (i) lower operating frequencies and (ii) inefficient use of area (on silicon). In this work, we propose an RV framework called faRM-LTL, that overcomes these two disadvantages by keeping the design of the runtime monitor unchanged even if the input properties change, thereby making it amenable for an ASIC implementation. We achieve this using a Linear Temporal Logic (LTL) Monitoring Instruction Set Architecture (LM-ISA), a compiler that translates properties specified in LTL into a sequence of LM-ISA instructions, and an associated programmable hardware runtime monitor that implements the LM-ISA. The flexibility of the faRM-LTL Monitor was evaluated on 53 LTL properties from several prior works. We also implemented the Monitor on an ASIC and found its area overhead to be under \(0.5\%\).

We propose an efficient offline monitoring algorithm for properties written in DMTL (Dynamic Metric Temporal Logic), a temporal formalism that combines MTL (Metric Temporal Logic) with regular expressions. Our algorithm has worst-case running time that is polynomial in the size of the temporal specification and linear in the length of the input trace. In particular, our monitoring algorithm needs time \(O(m^3 \cdot n)\), where m is the size of the DMTL formula and n in the length of the input trace.

First-order monitors analyze data-carrying event streams. When event streams are generated by distributed systems, it may be difficult to ensure that events arrive at the monitor in the right order. We develop a new monitoring tool for metric first-order temporal logic, called TimelyMon, that can process out-of-order events. Using the stream processing framework Timely Dataflow, TimelyMon also supports parallelized monitoring. We demonstrate TimelyMon’s good performance and scalability on synthetic and real-world benchmarks.

Stream Runtime Verification (SRV) is gaining traction for monitoring systems with data streams, but it struggles with specifying state-based systems and control flow. While automata models like state charts excel at representing states, functional languages offer solutions like monads (e.g., in Haskell) to elegantly handle state and data streams together. Other approaches exist in Lustre/Esterel or Rust. However, for SRV frameworks like TeSSLa, no such approach exists so far. This paper extends TeSSLa’s syntax by building on a monadic type to simplify for improved control flow specifications.

Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input exists that will generate a given interval.

By excluding data from the language, we obtain polynomial-time algorithms for the evaluation problem and for satisfiability when only considering inclusive rules. Furthermore, we show decidability for the satisfiability problem for cycle-free specifications and undecidability for satisfiability of full data-free nfer.

Runtime monitoring facilitates human oversight of safety-critical systems by collecting and aggregating data from sensors and other system components and by issuing alerts whenever the safety specification is violated. It is critical that the collected data is presented in a way that helps the user to quickly assess the situation. Most monitoring tools have only limited support for data visualization. We present RTLolaMo\(^{3}\)Vis, an online runtime monitoring framework that is mobile, modular, and supports the graphical visualization of the monitoring data in real time. RTLolaMo\(^{3}\)Vis is highly configurable, from data collection to the final visualization, which makes it applicable to a wide spectrum of applications. The design of RTLolaMo\(^{3}\)Vis follows the monitoring-based visualization approach, which minimizes the additional code for visualization by preprocessing the data in the monitor. We demonstrate the modularity and efficiency of RTLolaMo\(^{3}\)Vis on simulated drone flights and real-world communication data. On standard mobile phones and tablet computers, RTLolaMo\(^{3}\)Vis processes the monitoring output at a frequency of 100 Hz without any data loss.

Neural networks are increasingly used in safety-critical applications such as robotics and autonomous vehicles. However, the deployment of neural-network-controlled systems (NNCSs) raises significant safety concerns. Many recent advances overlook critical aspects of verifying control and ensuring safety in real-time scenarios. This paper presents a case study on using POLAR-Express, a state-of-the-art NNCS reachability analysis tool, for runtime safety verification in a Turtlebot navigation system using LiDAR. The Turtlebot, equipped with a neural network controller for steering, operates in a complex environment with obstacles. We developed a safe online controller switching strategy that switches between the original NNCS controller and an obstacle avoidance controller based on the verification results. Our experiments, conducted in a ROS2 Flatland simulation environment, explore the capabilities and limitations of using POLAR-Express for runtime verification and demonstrate the effectiveness of our switching strategy.

Since neural networks can make wrong predictions even with high confidence, monitoring their behavior at runtime is important, especially in safety-critical domains like autonomous driving. In this paper, we combine ideas from previous monitoring approaches based on observing the activation values of hidden neurons. In particular, we combine the Gaussian-based approach, which observes whether the current value of each monitored neuron is similar to typical values observed during training, and the Outside-the-Box monitor, which creates clusters of the acceptable activation values, and, thus, considers the correlations of the neurons’ values. Our experiments evaluate the achieved improvement.

Deep neural networks (DNNs), despite their impressive performance in various tasks, often produce overconfident predictions on out-of-distribution (OoD) data, which can lead to severe consequences, especially in safety-critical applications. Monitoring OoD samples for DNNs at runtime is thus essential. Although this problem has been extensively studied in image classification and recently in object detection with the Faster R-CNN architecture, the state-of-the-art series of You Only Look Once (YOLO) remains underexplored. This short paper presents an initial exploration into OoD detection for YOLO models, proposing a box-based monitor approach. The core idea is to use a data structure with a geometric shape of boxes to enclose regions in the logit space where the neural network makes decisions on in-distribution (ID) data. This structure serves as a reference to monitor the behavior of the network during deployment. Our preliminary results demonstrate that this box-based monitor outperforms several existing logits-based scoring methods, achieving a significant \(20\%\) reduction in false positive rates for OoD samples while maintaining a high true positive rate for ID samples. We hope that our work will spark meaningful discussion and inspire future research efforts, highlighting both the potential and the challenges of integrating OoD detection with the YOLO architecture for effective runtime monitoring.

In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.

An asynchronous, fault-tolerant, sound and complete algorithm for runtime verification of linearizability of concurrent algorithms was proposed in [7]. This solution relies on the snapshot abstraction in distributed computing. The fastest known snapshot algorithms use complex constructions, hard to implement, and the simplest ones provide large step complexity bounds or only weak termination guarantees. Thus, the snapshot-based verification algorithm is not completely satisfactory. In this paper, we propose an alternative solution, based on the collect abstraction, which can be optimally implemented in a simple manner. As a final result, we offer a simple and generic methodology that takes any presumably linearizable algorithm and produces a lightweight runtime verified linearizable version of it.

In distributed systems with processes that do not share a global clock, partial synchrony is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an approximate distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples.