Prof. Dr. Paula Herber, Institut für Informatik

Cyber-physical systems are systems that combine discrete control (or cyber) aspects with physical aspects. We can find examples of such systems in cars, airplanes, or water supply systems. With the current trend towards self-driving cars and smart infrastructures, these systems are becoming increasingly autonomous. This means that they use learning to take good control decisions in unforeseen situations and 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. Thus, the correctness and reliability of these systems are of vital importance. Formal verification techniques, which establish correctness using rigorous mathematical methods, can provide us with guarantees about crucial safety properties of cyber-physical systems. However, formal verification is known to be enormously expensive. Techniques for automatic verification explore the underlying state space of a given system, which is often too large to be fully explored. Deductive verification techniques provide a powerful solution to this problem by leveraging abstract mathematical reasoning, but they require tremendous effort and expertise to provide the necessary abstractions and proof ideas to guide the verification process. This problem is especially severe for autonomous cyber-physical systems, because the trial-and-error processes and statistical methods that are commonly used in learning are hard to capture formally.The main goal of this project is the safe integration of learning in autonomous cyber-physical systems with acceptable effort. Our key concept to achieve this is reusability. In particular, we investigate reusable abstractions for autonomous cyber-physical systems. By providing novel concepts for systematic reuse of formal specifications and abstractions (for example, property and specification patterns), we will significantly reduce the required manual effort and expertise, and thus increase the applicability and acceptance of deductive verification in industrial design processes for autonomous cyber-physical systems.