Verifying the safety of latency-aware cyber-physical systems is both critical and challenging due to the interaction between continuous physical dynamics and discrete computational constraints. This paper introduces SOTERIA, a formal framework that integrates digital twins for ensuring safety in these systems. SOTERIA models both the physical dynamics and computational behavior, enabling integrated verification within a specific operating environment. This approach goes beyond conventional methods that either treat physical and computational aspects separately or rely on overly conservative worst-case analyses. By modeling hybrid dynamics alongside computational models and operating environments, SOTERIA verifies both functional and timing correctness. Leveraging established verification tools, SOTERIA determines whether end-to-end latencies meet formal specifications, bridging the gap between computational and physical requirements. We first introduce a simple example of a 1D adaptive cruise control system to illustrate its effectiveness. We then present findings from a case study using the F1Tenth racing car platform and the UPPAAL tool to demonstrate SOTERIA's effectiveness in realistic scenarios, enabling safety verification that was previously infeasible with conventional schedulability analyses. This work underscores the importance of an integrated verification approach for enhancing safety and reliability in autonomous systems.

Autonomous systems are increasingly used in safety-critical domains, including industrial automation, autonomous vehicles, and the industrial Internet of Things. Verifying both the functional and temporal correctness of these systems is essential to ensure safety before deployment. However, end-to-end verification is challenging due to the interaction of continuous-time physical processes with discrete-time computational systems. Existing formal methods often assume simplified or static computational models, while traditional real-time systems focus on meeting timing constraints without explicitly linking them to physical safety. We address this gap by proposing a physics-informed mixed-criticality (MC) verification framework for cyber-physical systems, which allows the integration of computational and physical models for dynamic, fine-grained safety assurance. Our framework incorporates feedback from the local environment to guide criticality-based mode switching, ensuring adaptive responses to real-time physical states rather than relying on global worst-case assumptions. We demonstrate the feasibility of our approach with a prototype implementation on an autonomous F1 Tenth vehicle using preemptive EDF scheduling on ROS 2. Verification is conducted using UPPAAL to validate system behavior, mode transitions, and physical safety constraints. Results show that our framework effectively manages MC requirements, enhancing responsiveness and safety in dynamic environments.

Autonomous systems are heavily used in many safety-critical systems, such as industrial automation, autonomous cars, Industrial Internet of Things (I-IoT), etc. Verification of the functional and temporal correctness of such systems is necessary before deployment to ensure their safety. However, due to the presence of physical systems in the continuous-time domain and computational models in the discrete-time domain, end-to-end verification of these systems is highly challenging. Existing formal methods focus on verifying physical models assuming static or simplified computation models. In contrast, existing real-time systems focus on satisfying strict timing bounds but do not care how those bounds are obtained and how they relate to physical safety. Our approach bridges these two domains, and constitutes an end-to-end verification framework for arbitrary physical models and computational models incorporated within a cyber-physical automated system. By allowing the interaction between the computational and physical models, our verification framework enables a fine-grained scheme that verifies against the local environment instead of verifying against global worst-case assumptions. Moreover, to support locally varying worst-case scenarios, a mixed-criticality system is proposed where the system supports several critical models and switches among the modes based on environmental uncertainty. Finally, a proof-of-concept evaluation of the proposed framework is reported.

The second generation of robot operating system (ROS 2) received significant attention from the real-time system research community, mostly aiming at providing formal modeling and timing analysis. However, most of the current efforts are limited to the default scheduling design schemes of ROS 2. The unique scheduling policies maintained by default ROS 2 significantly affect the response time and acceptance rate of workload schedulability. It also invalidates the adaptation of the rich existing results related to nonpreemptive (and limited-preemptive) scheduling problems in the real-time systems community to ROS 2 schedulability analysis. This article aims to design, implement, and analyze a standard dynamic priority-based real-time scheduler for ROS 2 while handling shared resources. Specifically, we propose to replace the readySet with a readyQueue, which is much more efficient and comes with improvements for callback selection, queue updating, and a skipping scheme to avoid priority inversion from resource sharing. Such a novel ROS 2 executor design can also be used for efficient implementations of fixed priority policies and mixed-policy schedulers. Our modified executor maintains the compatibility with default ROS 2 architecture. We further identified and built a link between the scheduling of limited-preemption points tasks via the global earliest deadline first (GEDF) algorithm and ROS 2 processing chain scheduling without shared resources. Based on this, we formally capture the worst-case blocking time and thereby develop a response time analysis for ROS 2 processing chains with shared resources. We evaluate our scheduler by implementing our modified scheduler that accepts scheduling parameters from the system designer in ROS 2. We ran two case studies-one using real ROS 2 nodes to drive a small ground vehicle, and one using synthetic tasks. The second case study identifies a case where the modified executor prevents priority inversion. We also test our analysis with randomly generated workloads. In our tests, our modified scheduler performed better than the ROS 2 default. Our code is available online:https://github.com/RTIS-Lab/ROS-Dynamic-Executor.

Real-time machine learning object detection algorithms are often found within autonomous vehicle technology and depend on quality datasets. It is essential that these algorithms work correctly in everyday conditions as well as under strong sun glare. Reports indicate glare is one of the two most prominent environment-related reasons for crashes. However, existing datasets, such as the Laboratory for Intelligent & Safe Automobiles Traffic Sign (LISA) Dataset and the German Traffic Sign Recognition Benchmark, do not reflect the existence of sun glare at all. This paper presents the GLARE (GLARE is available at:https://github.com/NicholasCG/GLARE_Dataset) traffic sign dataset: a collection of images with U.S-based traffic signs under heavy visual interference by sunlight. GLARE contains 2,157 images of traffic signs with sun glare, pulled from 33 videos of dashcam footage of roads in the United States. It provides an essential enrichment to the widely used LISA Traffic Sign dataset. Our experimental study shows that although several state-of-the-art baseline architectures have demonstrated good performance on traffic sign detection in conditions without sun glare in the past, they performed poorly when tested against GLARE (e.g., average mAP0.5:0.95 of 19.4). We also notice that current architectures have better detection when trained on images of traffic signs in sun glare performance (e.g., average mAP0.5:0.95 of 39.6), and perform best when trained on a mixture of conditions (e.g., average mAP0.5:0.95 of 42.3).

Robot Operating System (ROS) is the most popular framework for developing robotics software. Typically, robotics software is safety-critical and employed in real-time systems requiring timing guarantees. Since the first generation of ROS provides no timing guarantee, the recent release of its second generation, ROS2, is necessary and timely, and has since received immense attention from practitioners and researchers. Unfortunately, the existing analysis of ROS2 showed the peculiar scheduling strategy of ROS2 executor, which severely affects the response time of ROS2 applications. This paper proposes a deadline-based scheduling strategy for the ROS2 executor. It further presents an analysis for an end-to-end response time of ROS2 workload (processing chain) and an evaluation of the proposed scheduling strategy for real workloads.