Cyber-physical systems pose particular challenges for formal verification: they are heterogeneous, interact with their physical environment, and must operate reliably even in the presence of uncertainty and unforeseen events. We investigate methods for bridging the gap between industrial modeling approaches, such as MATLAB/Simulink, and formal verification techniques. To this end, we develop approaches for transforming existing models into formally precise representations and systematically analyzing their correctness and safety using deductive verification and quantitative analysis techniques.

In embedded systems, hardware and software are tightly integrated, and systems often have to meet strict real-time requirements. Their formal verification poses significant challenges in terms of scalability and the effort required to develop suitable specifications. A key focus of our research is the automated transformation of informal system descriptions, such as those written in SystemC, as well as software for real-time operating systems such as FreeRTOS, into formal models. Furthermore, we develop novel approaches to enable scalable verification of these systems, for example by combining techniques from model checking and deductive verification.

Embedded systems often process sensitive information that must be protected against unauthorized access. Moreover, unauthorized access to safety-critical components, such as a vehicle's control system, can have serious consequences. We investigate methods for analyzing and securing information flow that account not only for data dependencies but also for timing dependencies and concurrent processes. A particular focus lies on analyzing complex interactions between concurrent processes and asynchronous external events, enabling the analysis of secure information flow even in embedded real-time systems.