InnoTrans 2012: Wir beweisen, dass Ihre Software richtig reagiert!

Meldung vom Di., 04. September 2012

Software steuert in der Bahntechnik immer mehr zentrale Funktionen, wie z. B. Fahrzeugtüren, Bremsen oder den Sicherheitsfahrschalter. Die Forscher von Fraunhofer FOKUS zeigen auf der InnoTrans 2012 (Halle 4.1, Stand 225) wie sich mit deduktiven Verifikationsverfahren beweisen lässt, dass die Software von solchen sicherheitskritischen Systemen fehlerfrei funktioniert.

Software steuert in der Bahntechnik immer mehr zentrale Funktionen, wie z. B. Fahrzeugtüren, Bremsen oder den Sicherheitsfahrschalter. Die Forscher von Fraunhofer FOKUS zeigen auf der InnoTrans 2012 (Halle 4.1, Stand 225) wie sich mit deduktiven Verifikationsverfahren beweisen lässt, dass die Software von solchen sicherheitskritischen Systemen fehlerfrei funktioniert.

Während der Fahrt muss ein Lokführer in regelmäßigen Abständen den sogenannten Sicherheitsfahrschalter (Sifa) betätigen. Tut er dies nicht, erfolgt nach einer optischen und akustischen Warnung eine Zwangsbremsung des Zuges. Dieses, umgangssprachlich auch als Totmannschalter bezeichnetes System soll verhindern, dass ein Zug über längere Zeit führungslos unterwegs ist. Solche sicherheitskritischen Systeme werden von Software gesteuert, die einwandfrei funktionieren muss, damit Risiken für Fahrgäste und Betreiber ausgeschlossen werden können. Bisher wurde die Verlässlichkeit der Software durch umfangreiche und zeitaufwändige Testverfahren überprüft. Mit zunehmender Größe und Komplexität sowie neuen Anforderungen von Qualitätsstandards wie der EN 50128 stoßen gängige Testverfahren aber an ihre Grenzen.
Die Wissenschaftler von Fraunhofer FOKUS haben daher im DEVICE-SOFT Projekt erforscht, wie sich die Eigenschaften von Software mit deduktiven Verifikationsverfahren beweisen lassen. Dabei werden mithilfe einer formalisierten Dokumentation der Software-Anforderungen und prädikatenlogischen Formeln die Vor- und Nachbedingungen einzelner Programmfunktionen definiert. Anschließend wird mit automatisierten Verfahren bewiesen, dass das Programm bei Einhaltung der Vorbedingungen die spezifischen Nachbedingungen erfüllt.
Bisher fehlte die Anwendung dieser Methoden für eingebettete Software in sicherheitskritischen Systemen, die mit industrieüblichen Programmiersprachen wie C oder C++ entwickelt wurden. Im Projekt untersuchten die Forscher daher, wie sich deduktive Verifikationsmethoden in industriellen, sicherheitskritischen Anwendungen breiter einsetzen lassen. Die Erfahrungen haben gezeigt, dass sie das Potenzial zur Verringerung der Verifikationskosten haben. Sie erleichtern darüber hinaus die Zulassung von Software in der Bahntechnik, da sich mit ihnen die Eigenschaften von sicherheitskritischer Software beweisen lassen.
Fraunhofer FOKUS ist eines der wenigen Institute, das über praktische Erfahrungen beim Einsatz deduktiver Verifikationsverfahren verfügt und seine Kunden beim Einsatz entsprechender Werkzeuge beraten kann.

Besuchen Sie uns vom 18.-21. September 2012 auf der InnoTrans in Halle 4.1, Stand 225. Gerne vereinbaren wir vorab einen Termin mit Ihnen.