Description

About 98% of the computing devices produced worldwide these days are used in embedded systems. The functionality spans from simple microcontrollers in a fridge to complex systems with millions of lines of code, for example in cars, airplanes, or smart factories. In such systems, failure often has serious consequences, such as huge financial losses or even loss of lives. Thus, the correctness and reliability of embedded systems are of vital importance.

To ensure the correct functioning of embedded systems, a clear understanding of the models and languages that are used in the development process is highly desirable. Formal methods provide a basis to make the development process systematic, well-defined, and automated. However, for many industrially relevant languages and models, the semantics is only informally defined. Together with the restricted scalability of formal design and verification techniques, this makes the formal verification of embedded control systems a major challenge.

This holds especially for embedded systems with open parameters, e.g. without a fixed number of components or with arbitrary sensor values, as those may cause unbounded state spaces. However, in the context of dynamically changing environments like we have for autonomous driving or smart factories, open parameters are highly desirable, as they significantly increase the flexibility of embedded control systems.

At the same time, we see that in the area of deductive program verification, powerful techniques and tools have been developed to reason about software with unbounded parameters. In this project, we will extend these techniques to make them suitable for embedded systems.

The goal of this project is to investigate how existing deductive verification techniques for concurrent software can be adapted to make them usable for parameterized embedded control systems that consist of both hardware and software and have possibly unbounded state spaces. This enables reasoning about both the data and control flow of such systems, and thus the verification of both functional and non-functional properties.

The project will be co-supervised by Prof. Dr. Paula Herber (Munster), who is an expert in formal analysis of embedded systems, and Prof. Dr. Marieke Huisman, who is an expert in deductive program verification.