Ein Algorithmus für alle Fälle

Unsere Computerprogramme werden ständig komplexer und dadurch anfälliger für Fehler. Sie zu finden und zu beheben erfordert viel Zeit – und die ist in der Praxis meist nicht vorhanden. Die Informatikerin Monika Henzinger sucht nach einer Lösung – und zwar in Form von superschnellen Algorithmen.

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."

uni:view: Frau Henzinger, wie beantworten Sie unsere aktuelle Semesterfrage: Wie leben wir in der digitalen Zukunft?
Monika Henzinger: In der digitalen Zukunft leben wir vernetzter: indem wir immer mehr Daten von uns preisgeben. Die Frage ist, ob wir das wollen. Im Moment gehen wir mit unseren Daten zu sorglos um. Ich wünsche mir, dass beispielsweise Apps, die abfragen, welche Daten wir freigeben wollen und welche nicht – und die bei einem "Nein" nicht jegliches Service unterbinden, sondern Zwischenstufen anbieten. Dafür müssten die Anwendungen verstärkt auch in Europa entwickelt werden, da hier das Bewusstsein für Datenschutz stärker ist. Unsere Gesellschaft wird in Zukunft zweigeteilt sein: Auf der einen Seite stehen die Menschen, die Bescheid wissen und bewusst mit Daten umgehen, und auf der anderen Seite jene, die das nicht machen und sich dadurch unterschiedlichen Gefahren aussetzen. Ich selbst bin z.B. nicht auf Facebook und WhatsApp benutze ich nur sehr diskret – versende also keine Bilder und keine Namen.

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.

VERANSTALTUNGSTIPP:

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.