As from 1 January 2021, Philip will work on the SAVES project: 'Scalable Verification of Industrial Embedded Control Systems'.
This project is a cooperation of WWU-Münster and the University of Twente, funded by a WWU - UT collaboration grant.
Embedded systems surround us everywhere in our everyday live. Their 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 establish correctness of embedded systems, however, is hard. With trends such as Industry 4.0, the internet of things, and autonomous driving, the complexity of embedded systems is steadily increasing. A prerequisite to ensure the correct functioning of industrial embedded systems under all circumstances is a clear understanding of the models and languages that are used in the development process. 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 are only informally defined. Together with the limited scalability of formal design and verification techniques, this makes the formal verification of industrial embedded control systems a difficult challenge, which can not be solved satisfactory with currently available methods and tools. 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, for example the VerCors tool suite. In this project, we will extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for industrial embedded systems.