Es ist allgemein anerkannt, dass die Bedeutung von eingebetteten Systemen in den nächsten Jahren steigen wird und sie in immer mehr Bereichen Anwendung finden. Bei sicherheitskritischen Anwendungen müssen eingebettete Systeme sehr hohen Auflagen genügen. Dies gilt insbesondere für die Luft- und Raumfahrt, den Medizinbereich, das Bahnwesen und auch die Automobilindustrie. In solchen Systemen können Fehler katastrophale Folgen in finanzieller Hinsicht haben oder sogar Menschenleben gefährden.

Um die Verlässlichkeit eingebetteter Software zu überprüfen, haben sich traditionelle Testmethoden für kritische Fälle als zu teuer erwiesen. Es ist sehr aufwändig, die notwendige hohe Testabdeckung zu erzielen. Hinzu kommt, dass in Zukunft die Größe und Komplexität eingebetteter Software noch zunehmen werden.

Eine Alternative stellen mathematische Methoden dar, die die erwünschten Sicherheitsbestandteile in der Software formal überprüfen. Diese Methoden, insbesondere der Hoare-Kalkül, sind wissenschaftlich eingehend untersucht worden. Allerdings fehlt bislang noch weitestgehend die Anwendung dieser Methoden für eingebettete Software, die in industrieüblichen Programmiersprachen entwickelt wurde. Daher ist es das Hauptziel des DEVICE-SOFT Projekts, deduktive Verifikationsmethoden für industrielle Anwendungen mit sicherheitskritischen eingebetteten Systemen nutzbar zu machen und dabei diese Methoden zu verbessern und weiter zu verbreiten.

Das Projekt stützt sich dabei auf das Frama-C-Framework und seine deduktiven Verifikations-Plug-Ins. SQC hat bereits viel Erfahrung in der Anwendung dieser Softwarewerkzeuge gesammelt und arbeitet in diesem Projekt mit dem Hauptentwickler von Frama-C, CEA List, zusammen.

Das Projekt wird im Rahmen der Fraunhofer-Carnot-Initiative vom Bundesministerium für Bildung und Forschung (BMBF) sowie der Agence Nationale de la Recherche (ANR) mit rund 575.000 Euro gefördert.