Cyber-physical systems form the foundation of numerous safety-critical applications, ranging from energy supply to autonomous robots and self-driving vehicles. In the DFG-funded project SApPHIRe (Systematic Approach for Provably correct Hybrid systems that are Intelligent and Resilient), we investigate novel formal methods to ensure the safety, performance, and resilience of these systems, even under uncertainty. To this end, we combine deductive verification with quantitative analysis techniques and develop approaches for the safe integration of learning-based components. Our goal is to efficiently analyze complex systems and establish their correctness through rigorous mathematical methods.

Embedded control systems combine discrete and continuous behavior and are often designed using model-based development tools such as MATLAB/Simulink. However, the semantics of the modeling languages used are often only informally defined. To mathematically establish the safety of such systems, we have developed a formally grounded approach to their modeling and verification. To this end, we transform Simulink models into formally precise representations of hybrid systems, enabling their mathematical verification using differential dynamic logic and the theorem prover KeYmaera X.

Autonomous cyber-physical systems increasingly rely on learning-based techniques to make decisions independently in dynamic environments. While learning significantly increases their flexibility, it also increases their complexity. At the same time, failures often have serious consequences in cyber-physical systems, as they may cause huge financial losses or even loss of lives. In the DFG-funded project SafeILIAS (Safe Integration of Learning In Autonomous cyber-physical Systems), we develop methods for safely integrating learning components into these systems. By introducing reusable specifications and formal abstractions, we aim to reduce verification effort and facilitate the systematic verification of safety in autonomous systems.

Embedded control systems are used in a wide range of industrial applications and are becoming increasingly complex. Their formal verification poses significant challenges, particularly due to the interaction of heterogeneous components, concurrent processes, and real-time requirements. In the SAVES (ScAlable Verification of Embedded Systems) project, we collaborate with researchers at the University of Twente to develop methods and tools that make the mathematical verification of such systems more efficient and scalable. To this end, we extend deductive verification techniques to account for the specific characteristics of industrial embedded systems and systematically establish their correctness.

Embedded systems combine complex hardware and software components and are often used in safety-critical applications. Their verification poses significant challenges in terms of scalability, particularly due to diverse models of computation and the interaction of heterogeneous components. In the DFG-funded project RESCUE, we developed methods that combine static analysis, program slicing, and various verification techniques to verify such systems more efficiently. To this end, models from industrial design tools such as SystemC and MATLAB/Simulink are automatically transformed into formally defined models. This enables existing verification tools to be applied in a targeted manner to analyze safety, liveness, and timing properties, as well as to investigate potential errors using counterexamples.

SystemC is a widely used modeling language for embedded hardware and software systems, but its semantics are not fully formally defined. The tool STATE (SystemC to Timed Automata Transformation Engine) automatically transforms SystemC models into timed automata for the UPPAAL model checker. The transformation is based on a formal semantics of SystemC and enables semantics-preserving translation into a formally defined model. The structure of the original design remains traceable, facilitating analysis and debugging. STATE supports, among other features, complex data structures, pointers, arrays, and the TLM-2.0 standard.