SAVES - Scalable Verification of Industrial Embedded Control Systems

this project is a cooperation of WWU 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 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. Automated 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 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 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.

Cooperation partner: University of Twente, Formal Methods and Tools Group

Principal Investigators: Prof. Dr. Marieke Huisman, Prof. Dr. Paula Herber
Involved Researchers: Philip Ben Heinrich Tasche, M.Sc. (PhD student)