Bahnfahren? Sicher!

Deduktive Verifikation für sicherheitskritische Software eingebetteter Systeme

In der Bahntechnik übernimmt die Software von eingebetteten Systemen immer mehr zentrale Steuerungsfunktionen. Sie steuert z. B. die Fahrzeugtüren oder löst die Bremsen aus, wenn der Sicherheitsfahrschalter nicht ordnungsgemäß betätigt wird. Bei sicherheitskritischen Systemen, wie z. B. Signalanlagen, muss die einwandfreie Funktion gesichert sein, um Risiken für Fahrgäste und Betreiber auszuschließen. // Quelle: FIRST

Bisher wurde die Verlässlichkeit der Bahntechnik Software durch umfangreiche und damit aufwändige und teure Tests überprüft. Auch die zunehmende Größe und Komplexität eingebetteter Software setzt gängigen Testverfahren Grenzen. Darüber hinaus stellen neue Qualitätsstandards wie EN 50128 zusätzliche Sicherheitsanforderungen an eingebettete Software.

Hier bieten deduktive Verfahren eine Alternative zu traditionellen Testmethoden: Die erwünschten Eigenschaften der Software werden formal mit sogenannten Unit-Beweisen belegt. Dazu benötigt man eine formalisierte Dokumentation der Anforderungen. Mithilfe von prädikatenlogischen Formeln werden die Vor- und Nachbedingungen für die einzelnen Programmfunktionen definiert. Anschließend wird mit automatisierten Verfahren bewiesen, dass das Programm bei Einhaltung der Vorbedingungen die spezifischen Nachbedingungen erfüllt.

Die zugrunde liegenden Methoden sind wissenschaftlich eingehend untersucht worden. Allerdings fehlte bislang noch die Anwendung dieser Methoden für eingebettete Software sicherheitskritischer Systeme, die in industrieüblichen Programmiersprachen, wie z. B. C oder C++, entwickelt wurde.

Fraunhofer FIRST untersucht im Projekt DEVICE-SOFT, wie sich deduktive Verifikationsmethoden für industrielle Anwendungen mit sicherheitskritischen eingebetteten Systemen breiter einsetzen lassen. Erste Erfahrungen zeigen, dass sie zu geringeren Validierungskosten führen und zuverlässiger sind als Softwaretests. Der Einsatz deduktiver Verfahren kann außerdem die Zertifizierung sicherheitskritischer Software in der Bahntechnik erleichtern, denn im Gegensatz zum Testen lässt sich mit ihnen beweisen, dass die Software die entsprechenden Anforderungen erfüllt.

Fraunhofer FIRST ist eines der wenigen Institute, das über praktische Erfahrung beim Einsatz deduktiver Verifikation verfügt und seine Kunden beim Einsatz entsprechender Werkzeuge beraten kann. Das Projekt DEVICE-SOFT wird im Rahmen der Fraunhofer-Carnot-Initiative vom Bundesministerium für Bildung und Forschung (BMBF) sowie der Agence Nationale de la Recherche (ANR) gefördert.

Besuchen sie uns auf der InnoTrans 2010 auf dem Messegelände Berlin. Sie finden uns in Halle 4.1, Stand 217.

Weitere Informationen:

Ronny Meier, Referent Institutskommunikation
Tel.: +49 (0) 30/ 6392-1814
Mobil: + 49 (0) 175/ 1850619
E-Mail: ronny.meier(at)first.fraunhofer.de

Ort und Zeit:

InnoTrans 2010 vom 21.-24. September auf dem Messegelände Berlin
Webseite der Messe InnoTrans 2010

Öffnungszeiten:
21.-24.09.2010 Fachmesse: 9:00 - 18:00 Uhr
25.-26.09.2010 Publikumstage: 10:00 - 18:00 Uhr

Pressemitteilung Nr. 130, 08.09.10
www.first.fraunhofer.de