ABSTRACT. Neural networks are increasingly used to control and make decisions in fields such as robotics and autonomous vehicles. Despite their effectiveness, the deployment of neural network-controlled systems (NNCSs) in safety-critical applications raises significant safety concerns. Recent advances in neural network verification and reachability analy- sis tools have begun to address these issues, yet the majority of these efforts focus on offline time-irrelevant verification tasks. This gap over- looks critical aspects of verifying control and ensuring safety in real-time scenarios. This paper presents a detailed case study on using a state- of-the-art NNCS reachability analysis tool, POLAR-Express, for run- time safety verification in a Turtlebot navigation system. The Turtlebot, equipped with a neural network controller for steering, operates in a com- plex environment with obstacles. Thus, we further developed a safe online controller switching strategy that switches between the original NNCS controller and an obstacle avoidance controller based on the verification results, to ensure safety and maintain control performance. Our exper- iments, conducted in a ROS2 Flatland simulation environment, explore the capabilities and limitations of using POLAR-Express for runtime verification in dynamic environments, and demonstrate the effectiveness of our switching strategy.

ABSTRACT. 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.

ABSTRACT. Deep neural networks, despite their impressive performance across 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 at runtime is thus essential. While 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 YOLO series remains underexplored. In this short paper, we present an initial exploration into OoD detection for YOLO models, proposing a box-based monitor approach. 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 in-distribution samples. This work introduces novel, yet not fully developed, ideas and emerging techniques in the realm of monitoring OoD inputs for YOLO series object detection models. Future research will focus on leveraging feature space information to enhance our results further. This paper aims to spark productive debate and provide impetus for future research, highlighting both the potential and the challenges of integrating OoD detection with the YOLO architecture for effective runtime monitoring.

ABSTRACT. In formal verification, monitoring consists in observing a system execution and deciding, as early as possible, whether it satisfies or violates 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 having 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 can not be perfectly synchronized, so these timestamps are imprecise. This entails that they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims at providing, as early as possible, a verdict on the property it is monitoring, based on its possibly incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line symbolic 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 which updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.

ABSTRACT. It was recently proposed an asynchronous, fault-tolerant, sound and complete algorithm for runtime verification of linearizability of concurrent algorithms. 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.

ABSTRACT. In distributed systems with processes that do not share a global clock, \emph{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 \emph{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 monitoring efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its effectiveness and efficacy in both real-world applications and synthetic examples.