Fehler im Programm

Informatiker entwickeln formale Methoden, die die Korrektheit von sicherheits­kritischen Hard- und Softwaresystemen gewährleisten.

Wenn im Büro der Computer mitten bei der Arbeit »abstürzt« und damit die Aufzeichnungen der letzten Tage verloren gehen, dann ist das zwar ein Grund zum Verzweifeln aber keine Katastrophe. Anders wäre es, wenn zum Beispiel in einem Airbus das elektronische Leitsystem aufgrund von Programmierfehlern versagte, und es dadurch zu einem Absturz der Maschine käme. Damit so etwas nicht passiert, müssen sicherheitskritische Hard- und Softwaresysteme auf Korrektheit geprüft werden. Der Experte spricht von »Programm-Verifikation«. Um die Zuverlässigkeit und Korrektheit von Programmen zu garantieren, reicht es nicht aus, sie nur zu testen, sondern es wird eine formale Verifikation, das heißt eine Überprüfung mit mathematisch exakten Mitteln, benötigt. Solche Verifikationsbeweise sind im Allgemeinen sehr aufwändig, insbesondere bei umfangreichen Programmen, wie sie in der Praxis eingesetzt werden. Aus diesem Grund wird versucht, die Aufgabe der Verifikation weit gehend automatisch durchzuführen.

Am Institut für Informatik befasst sich der Lehrstuhl für Softwaretechnologie mit dieser Aufgabe. Eingebunden in nationale und internationale Projekte entwickelt das Team um Professor Willem-Paul de Roever neue Methoden und Software für die Programm-Verifikation. Der Schwerpunkt liegt hierbei auf Programmen, die in der Programmiersprache JAVA geschrieben sind, und auf Sprachen für programmierbare Speicherbausteine (PLCs). Solche Bausteine benutzt man zum Beispiel, um die Kontrolle von industriellen Prozessen zu automatisieren. Aktuell arbeiten die Kieler Informatiker unter anderem im Verbund »OMEGA« mit, bei dem auch Partner aus den Niederlanden, Frankreich und Israel beteiligt sind. Ziel von OMEGA ist es, eine Methodik zur Programmentwicklung in UML (Unified Modeling Language) zu definieren, die formale Techniken zur Überprüfung von eingebetteten Systemen und Echtzeitsystemen beinhaltet. Die entwickelten Methoden und Techniken werden in vier Fallstudien bei den Industriepartnern evaluiert, um ihre Anwendbarkeit in der Praxis zu überprüfen. Die Fallstudie der EADS Space Transportation zum Beispiel untersucht die Flugkontroll-Software der europäischen Trägerrakete Ariane 5-Raumfähre, die Fallstudie der Israelischen Luftfahrtindustrie (IAI) testet einen Flugkontrollmechanismus.

Professor de Roever ist davon überzeugt, dass »das Schreiben von zuverlässiger Software ein entscheidender Faktor für das Überleben der deutschen Industrie, vor allem der Autoindustrie, sein wird.« Die Software der Autos wird gewöhnlich von Zulieferbetrieben produziert. Wie diese Software funktionieren soll, werde jedoch nicht ausreichend präzise beschrieben. Die Folge, so de Roever: »Wenn Software und Hardware zusammengesetzt werden, kommt es zu unvorhersehbaren Ereignissen, zum Beispiel öffnet sich der Kofferraum oder der Zündschlüssel springt während der Fahrt aus dem Zündschloss. Zur Lösung der Probleme stellen Autohersteller mittlerweile Expertenteams zusammen, die herausfinden sollen, was genau die gelieferte Software macht und ob sie mit der Hardware der Autos, für die sie entwickelt wurde, zusammenpasst.«

Über die Zukunft der Doktoranden am Lehrstuhl braucht sich de Roever keine Sorgen zu machen. Kai Baukus, der gerade seine Dissertation abgeschlossen hat, arbeitet in einem Expertenteam bei BMW, das die Korrektheit der gelieferten Software überprüft. Ein anderer, Ben Lukoschus, testet Software für den Airbus A380. Die Firma, für die er arbeitet, wurde von Professor Jan Peleska gegründet, der sich am Lehrstuhl habilitiert hat. »Das zeigt«, so de Roever, »dass die Programm-Verifikation in Deutschland den Sprung zur industriellen Anwendung gemacht hat.« ne

Zuständig für die Pflege dieser Seite: Pressestelle der Universität, presse@uv.uni-kiel.de