A Systematic Approach for Provably correct Hybrid systems that are Intelligent and Resilient (SApPHIRe)

Cyber-physical systems (CPS) play an increasingly critical role in modern society. They are used in complex safety-critical applications, ranging from essential infrastructures like energy and water supply to autonomous systems such as robots and self-driving vehicles. Ensuring the safety, performance, and resilience of CPS is a major challenge, in particular for the following reasons: First, CPS are hybrid systems in the sense that they combine discrete and continuous behavior. Second, CPS are subject to uncertainties such as sensor noise or failures. Third, CPS increasingly use learning to take intelligent control decisions in dynamic environments. Compositional formal methods like deductive verification enable modular verification of rigorous correctness guarantees. However, they often ignore real-world uncertainties or rely on overly conservative assumptions. Quantitative model-based evaluation techniques, such as statistical model checking or reachability analyses for stochastic hybrid systems, provide probabilistic guarantees. However, they are limited to specific system classes and time-bounded properties. The project SapPHIRe – A Systematic Approach for Provably Correct Hybrid Systems that are Intelligent and Resilient aims to bridge the gap between these fundamentally different approaches by developing new methodologies that enable the compositional and quantitative verification of hybrid systems under uncertainty. SapPHIRe introduces three key ideas: (1) novel modeling techniques that formally capture system uncertainties in a way compatible with both deductive verification and quantitative evaluation, (2) new methods for decomposing complex system-level requirements into manageable, context-sensitive service levels to support scalable compositional reasoning over quantitative properties, and (3) strategies for safely integrating learning components. This research lays the groundwork for intelligent and resilient CPS that are not only capable but also provably correct.