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 life. Their functionality spans from simple micro-controllers 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. Formal, mathematically founded, 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. Auto-mated transformations into formal languages provide a solution for this, for example, the STATE tool developed at the WWU Münster. However, the limited scalability of formal design and verification techniques still makes the formal verification of industrial embedded control systems a difficult challenge, which cannot 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 are developed to reason about software with unbounded parameters, for example the VerCors tool suite developed at the University of Twente. In this project, we extend these techniques with concepts to cope with heterogeneity, concurrency, and real-time to make them suitable for industrial embedded systems. The result of the SAVES project will be an open source framework for scalable verification of industrial embedded control systems.
SAVES is a joint project of Prof. Dr. Marieke Huisman, head of the Formal Methods and Tools group at the University of Twente, and Prof. Dr. Paula Herber, head of the Embedded Systems group at the WWU Münster. It is funded from Jan. 2021 - Dec. 2022 by a WWU-UT collaboration grant. Dr. Raúl Monti works as a postdoc in the project, Philip Tasche as a doctoral student, and Pauline Blohm as a student assistant.
Principal Investigators:
INVOLved researchers:
