Ein Algorithmus für alle Fälle

Im Jahr 2015 stürzte ein Airbus über Spanien ab. Ursache des Absturzes war ein Softwareproblem. "Mindestens einmal jährlich passiert etwas Gröberes aufgrund eines Programmierfehlers – vom Ausfall von Kraftwerken oder Stromsystemen bis eben hin zu Flugzeugabstürzen", beschreibt Monika Henzinger das Problem: "Wir arbeiten daran, dass das in Zukunft nicht mehr – oder zumindest seltener – passiert."

Die Leiterin der Forschungsgruppe Theory and Applications of Algorithms an der Universität Wien forscht im Rahmen eines WWTF-Projekts an Algorithmen, um Software- und Hardwaresysteme in der Entwicklung zu verifizieren, damit solche Fehler zukünftig bereits im Vorfeld ausgeschlossen werden können. "Im Moment ist das leider nur für kleinere Systeme möglich. Umfassendere Programme – und wie wir wissen, werden Computer und Programme ständig komplexer – kann man hingegen noch nicht verifizieren", betont die Informatikerin.

Fehler finden über Nacht

Die Verifikation würde einfach viel zu lange – sprich Wochen oder gar Monate – dauern. In ihrer täglichen Praxis fehlt ProgrammiererInnen schlicht die Zeit, ihre Arbeit mit einem solchen Tool zu überprüfen.

"Die Entwicklerin schreibt einen neuen Teil bzw. eine Änderung eines Programms und checkt diesen am Abend ein – d.h. der neue Teil wird in das bestehende System eingefügt. Über Nacht lässt man große Testpakete mit verschiedenen Beispielen vom neuen Code lösen. Am nächsten Morgen sieht die Entwicklerin, ob eines dieser Beispiele eine falsche Antwort gibt oder nicht. Erst dann kann sie weiterarbeiten. Allerdings gibt es Fehler, die durch die bisherigen Testpakete nicht gefunden werden", beschreibt Henzinger einen typischen Arbeitsablauf, den sie mit ihrer Forschung optimieren will: "Würden über Nacht hingegen Verifikationstools laufen, könnten – unabhängig von bestehenden Testpaketen – mehr Fehler gefunden werden. Und daran forschen wir."

Algorithmen in die Schranken weisen

Während sie im vorhergehenden Projekt schnellere Algorithmen für "relativ einfache" Aufgaben entwickelt hat, befasst sie sich nun – gemeinsam mit ihrem Team – mit komplexeren Problemen. "Wir brechen die großen Fehler sozusagen in kleinere Arten von Fehlern herunter und versuchen, diese zu verifizieren", erklärt die Algorithmik-Expertin die Herangehensweise in für Laien verständlicher Sprache.

Dabei ist das Forschungsergebnis nicht immer ein neuer Algorithmus. "Manchmal stellen wir fest: Dieses Problem ist einfach nicht schneller lösbar – dann haben wir eine sogenannte 'untere Schranke' identifiziert", so die Informatikerin und erklärt: "Das heißt, wir haben formal bewiesen, dass es nicht schneller gehen kann. Dadurch ersparen wir anderen AlgorithmikerInnen viel Zeit: Sie brauchen nicht mehr länger nach einem schnelleren Algorithmus für dieses bestimmte Problem zu suchen – denn es gibt ihn nicht." Und dabei kann die Zeitersparnis enorm sein – immerhin wird an manchen Problemen bereits seit über 20 Jahren gearbeitet.

Monika Henzinger hat bereits etliche "untere Schranken" entwickelt und auf verschiedenen Konferenzen präsentiert – was in der Informatik übrigens mehr zählt als das Publizieren in einem Fachjournal.

Der Praxistest

Aber ein Algorithmus kann noch so schön laufen – wenn er zu kompliziert ist, kommt er in der Praxis nicht zur Anwendung. "Es wären dann bereits in der Implementierung zu viele Fehler möglich. Daher machen wir im angewandten Teil des Projekts den Praxistest – sprich eine Prototyp-Implementierung", erzählt die Projektleiterin und fügt ergänzend hinzu. "Wir demonstrieren, dass der Algorithmus nicht nur schnell, sondern auch implementierbar ist, und mit welcher Art von Problemen er gut funktioniert." Den Unternehmen bleibt es trotzdem nicht erspart, viel Hirnschmalz in die Anwendung zu stecken – immerhin muss der Algorithmus zur firmeneigenen Software passen.

Doch welche Firmen sind es, die in der Praxis mit den an der Universität Wien entwickelten Algorithmen arbeiten? "Etliche, aber das im Detail zu verfolgen, wäre zu viel Aufwand. Außerdem verraten das die Unternehmen ungern – damit würden sie ja Informationen freigeben, die schlussendlich der Konkurrenz nützen", antwortet die Informatikerin, der es als Wissenschafterin in erster Linie wichtig ist, von FachkollegInnen zitiert zu werden.

Vereinte Sphären der Informatik

Während die Entwicklung der Algorithmen das Spezialgebiet von Monika Henzinger ist, übernimmt den Part der Implementierung und der Verifikation ein Team vom IST Austria rund um Krishnendu Chatterjee, mit dem die Forschungsgruppe der Universität Wien erfolgreich kooperiert. "Eine solche Kooperation zwischen VerifikationsexpertInnen und AlgorithmikerInnen ist sehr ungewöhnlich – meines Wissens gibt es weltweit nur eine andere Forschungsgruppe in Israel", unterstreicht Henzinger die Besonderheit des aktuellen Projekts und erklärt: "Seit 30 Jahren arbeiten die beiden Bereiche getrennt voneinander – sie besuchen verschiedene Konferenzen und 'sprechen' jeweils eigene Sprachen."

Also müssen Henzinger und Chatterjee zunächst einmal gegenseitige Übersetzungsarbeit leisten, um am Ende gemeinsam den "First polynomial time algorithm" zu entwickeln. Also einen Algorithmus, der bei komplexen Problemen nicht exponenziell länger läuft und damit auch die Verifikation umfassender Programme in kurzer Zeit ermöglicht. Vereinfacht gesagt: einen schnellen Algorithmus, der in der Praxis gut funktioniert. (ps)

Das WWTF-Projekt "Efficient Algorithms for Computer Aided Verification" läuft von März 2016 bis März 2020 unter der Leitung von Univ.-Prof. Dr. Monika Henzinger, Leiterin der Forschungsgruppe Theory and Applications of Algorithms an der Universität Wien. Projektpartner sind: Krishnendu Chatterjee vom Institute of Science and Technology Austria (IST) sowie Dipl.-Ing. Dipl.-Ing. Dr. Wolfgang Dvorak von der Forschungsgruppe Theory and Applications of Algorithms an der Universität Wien. Projektmitarbeiterin ist Dipl.-Ing. Veronika Loitzenbauer von der Forschungsgruppe Theory and Applications of Algorithms.