Fehlerfreie Software als Ziel

Ein Problem, das es nach Ansicht von Experten nicht geben müsste. Und in vielen Anwendungen darf es Softwarefehler auch nicht geben, vor allem, wenn es um die Sicherheit geht. So müssen etwa Softwaresysteme in Fahrzeugen oder Flugzeugen extrem zuverlässig arbeiten – Ausfälle können dramatische Folgen haben. Teure Rückrufaktionen sind dabei noch das „kleinste“ Übel. Die Krux: Mit der zunehmenden Zahl an Elektronikkomponenten in den Autos steigt aber auch das Risiko von Pannen.

Wie man Software entwickelt, die garantiert fehlerfrei funktioniert, möchten Forscher der Universität des Saarlands in einem umfassenden Forschungsprojekt belegen. Ein Experte für das Thema „Fehlerfreie Software“ ist Holger Hermanns, Professor für Verlässliche Systeme und Software. Hermanns stellt klar: „Ein System ist verlässlich, falls man rechtfertigen kann, warum man sich auf dessen korrektes Funktionieren verlassen darf.“ Die Verlässlichkeit bezieht sich dabei auf die Zuverlässigkeit, Verfügbarkeit und Sicherheit eines Systems. Eigens dafür entwickelt das Forscherteam Methoden, mit denen man voraussagen kann, wie verlässlich die Eigenschaften eines Systems sind. Moderne Fahrzeuge verfügen über etwa 1000 Softwarefunktionen, mehrere Bordnetzwerke und mehr als 70 Steuergeräte. Die reine Zahl der Hardwareplattformen ist überdies trotz aller Bestrebungen nach Vereinheitlichung noch groß. Damit die komplexen Netzwerke pünktlich und zuverlässig reagieren, wollen die Forscher neue Verfahren entwickeln, die es erlauben, auch für komplexere Anwendungen Funktionsgarantien unter allen Umständen geben zu können. Im Mittelpunkt der Forschungen steht die automatische Fehlerdiagnose von Steuerungssystemen in Verkehrsmitteln. Die Sicherheit von verkehrstechnischen Anwendungen in Bereichen wie Auto, Flugzeug und Bahn soll dabei mit mathematischen Methoden nachgewiesen werden.

Auch das Saarbrücker Forschungsprojekt Verisoft XT beschäftigt sich mit der Analyse von sicherheitskritischen Systemen. Wenn bewiesen wird, dass Computersysteme ihre mathematisch exakten Vorgaben korrekt erfüllen, spricht man von formaler Verifikation. Die Methoden für die formale Verifikation von komplexen Computersystemen, die Soft- und Hardware umfassen, haben Wissenschaftler im Rahmen des Vorgängerprojekts Verisoft seit 2001 entwickelt. Das Ziel von Verisoft XT ist es jetzt, ein Qualitätssiegel „Verified in Germany“ zu erarbeiten und die Verifikation auf existierende Industrieprojekte anzuwenden. Für diese soll der mathematische und maschinell überprüfte Beweis erbracht werden, dass die betrachteten Computersysteme im Entwurf null Fehler enthalten. Verisoft XT, an dem auch der Branchenriese Microsoft beteiligt ist, wird seit 2007 vom Bundesministerium für Bildung und Forschung (BMBF) mit zwölf Millionen Euro gefördert.

An der Universität des Saarlandes geht man noch einen Schritt weiter. Man konzentriert sich nicht allein auf die Projekte, sondern berücksichtigt auch den Aspekt Mensch. Die Ausbildung der Fachrichtung Informatik wird darauf ausgerichtet, dass die Studenten von Beginn an lernen, wie fehlerfreie Softwaresysteme aufgebaut sein müssen. „Sie werden dafür – und das ist deutschlandweit einzigartig – bereits in den allerersten Pflichtvorlesungen damit vertraut gemacht, die Korrektheit ihrer Programme zu beweisen. Und dies zieht sich durch die weiteren Programmieraktivitäten des ganzen Studiums“, so Holger Hermanns gegenüber der Presse. Mit diesem Wissen könnten Softwarepannen wie bei Toyota oder anderen Unternehmen nach Ansicht der Experten verhindert werden.

Bild: Bosch