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.

Describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it to be correct.>