As from 1 January 2021, the SAVES project started.
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.
PRINCIPAL INVESTIGATORS:
PROF.DR. M. HUISMAN (MARIEKE)
Full Professor
Prof. Dr.PAULA HERBER
INVOLVED RESEARCHERS:
DR. R.E. MONTI (RAÚL)
Researcher
STEFANIE DRERUP
Master Thesis Student
