It is widely believed and accepted that embedded systems will continue to rise in their applicability and usage across numerous market sectors. However, in some cases, systems must satisfy stringent assurances, i.e., safety-critical requirements. In particular, these sectors include the aerospace, medical, railways, and potentially the automotive industry. In such systems, consequences of a failure can be disastrous, e.g., financially or even in terms of human lives.

Consequently, in these instances, it is very important that products demonstrate adherence to higher safety assurance levels. Traditional testing methods, for these classes of systems, have been shown to be too expensive. With traditional methods, reaching test-coverage that is appropriate when lives are at stake requires an ever bigger part of the development budget as embedded software grows in size and complexity. At these higher assurance levels, it may be more efficient to rely on mathematically rigorous methods that formally prove desired safety properties in software.

While such methods, particularly, Hoare logic-based deductive verification have been successfully studied from an academic point of view, their use in real-world applications, developed using contemporary programming languages for embedded software, remains largely undone. In this context, the main goal of the project is to disseminate, improve, integrate, and deploy deductive verification technologies into the industrial domain of safety critical embedded systems.

The project is centered around the Frama-C framework and its deductive verification plug-in. SQC has gained significant experience in the use of the tool and works with the main developer of Frama-C, CEA LIST, in order to guide the development of the Frama-C toward relevant real-world issues, and to foster its adoption by an increasingly larger community of users, by making them aware that this tool exists, and is able to tackle their software verification tasks.

DEVICE-SOFT is funded within the Fraunhofer-Carnot-Initiative by the Federal Ministry of Education and Research (BMBF) and the Agence Nationale de la Recherche (ANR), to the tune of approximately, EUR 575,000.