Im Sonderforschungsbereich AVACS haben Top-Informatiker vermeintlich „unentscheidbare“ Probleme in sicherheitskritischen Systemen beherrschbar gemacht. Im Interview blickt Sprecher Werner Damm auf spannende zwölf Jahre zurück.
FRAGE: Herr Damm, zwölf Jahre ist die Höchstdauer für einen Sonderforschungsbereich, Sie haben das voll ausgeschöpft. Offenbar geht es bei AVACS um ein komplexes Thema?
DAMM: Das kann man so sagen. AVACS steht für „Automatic Verification and Analysis of Complex Systems“ – der Begriff „komplexe Systeme“ steckt also schon im Titel. Konkret geht es um technische Anwendungen, die sicherheitsrelevant sind, also zum Beispiel die Elektronik in einem Flugzeug oder Auto. Nun ist AVACS kein Projekt des Bundesministeriums für Bildung und Forschung, sondern ein Sonderforschungsbereich. Daher hatten wir mitnichten vor, solche Systeme zu entwickeln. Wir wollten viel mehr die Komplexität, die wir am Markt beobachten, mathematisch beherrschbar machen, um beweisen zu können, dass die Systeme sicher sind. Das war das zentrale Anliegen von AVACS. Und wir haben es geschafft: Unsere Ergebnisse sind einfach erstaunlich.
FRAGE: Inwiefern?
DAMM: Die Informatik kennt die Begriffe „entscheidbar“ und „unentscheidbar“. Es gibt also Probleme, die nicht entscheidbar sind – da könnten Sie beliebig viel Rechenkapazität und ganz viele schlaue Köpfe zusammenbringen, es ist einfach nicht lösbar. Das kommt häufig vor bei Systemen, die nicht-linearen Differenzialgleichungen genügen: Selbst kleinste Änderungen können große Störungen verursachen. Wenn also beispielsweise ein Pilot ein wenig zu stark am Joystick zieht, dann kann das – wenn die Elektronik es nicht auffängt – zu einem extremen Steilflug führen. Bisher konnte man nicht formal nachweisen, dass solche Systeme sicher sind. Es war unentscheidbar. Dann kam AVACS – und wir haben gezeigt, dass es eben doch geht.
FRAGE: Wie ist das gelungen?
DAMM: Ich erkläre es mal an einem Beispiel: Nehmen wir das autonome Fahren. An einer Kreuzung müssen sehr viele Autos koordiniert werden, damit es nicht zu Unfällen kommt. Die Sicherheit dieser Systeme nachzuweisen ist nicht entscheidbar – es sind ja vom Grundgedanken her unbeschränkt viele Autos vorhanden. Man kann aber zum Beispiel hingehen und die unwichtigen Informationen ausblenden – beispielsweise die Kennzeichen der Autos. Dadurch wird das ganze System vereinfacht. Außerdem konnten wir – nicht zuletzt auch wegwn der Ausblendung der Kennzeichen – sogar mathematisch beweisen, dass es nicht nötig ist den Beweis für unbeschränkt viele Autos führen – es reicht , wenn ich ihn für eine bestimmte Anzahl erbringe. Wie viele das sein müssen, kann man aus den Sicherheitsanforderungen ableiten, das gibt es zum Beispiel Vorgaben wie viel Mindestabstand zwischen den Fahrzeugen sein muss. So wird ein vermeintlich unentscheidbares Problem entscheidbar. Das ist jetzt nur ein Beispiel. In AVACS haben wir mehrere solcher Aussagen treffen können, die wirklich bahnbrechend sind.
FRAGE: Das klingt nach einem Erfolg auf der ganzen Linie…
DAMM: Es könnte nicht besser sein. Wir können diese Ergebnisse nicht hoch genug bewerten. Sie sind nutzbar für alle technischen Systeme, in denen nicht-lineare Differenzialgleichungen relevant sind: Chemische Produktionsprozesse, die Steuerungen von Kernkraftwerken, die Stabilisierung von Energienetzen – man könnte mit diesen Methoden sogar analysieren, ob unsere Energieversorgung einer terroristischen Attacke standhalten kann. Das Geheimnis von AVACS war, dass wir da Köpfe zusammengetan haben, die einerseits etwas von den Anwendungen verstehen – wie in unserem Beispiel, dass der Steuerung eines Autos herzlich egal ist, welches Kennzeichen es hat – und andererseits die Modellbildung, also die notwendigen Beweisverfahren, beherrschen.
FRAGE: Und diese Kompetenzen gibt es alle hier in Oldenburg?
DAMM: Wir haben ein Team gebildet mit Wissenschaftlern aus Oldenburg, Saarbrücken und Freiburg, die aus sehr unterschiedlichen Ecken Beiträge lieferten. Hier in Oldenburg steckt die Kompetenz zur Modellbildung und das Anwendungs-Knowhow, in Saarbrücken gibt es sehr viel Wissen zu Echtzeitanalyse-Techniken und zur Wahrscheinlichkeitsrechnung, die Kollegen kennen sich zudem sehr gut mit Algorithmen und logischer Fundierung aus. Freiburg war unser Zentrum für Schaltungs-Verifikation und effiziente Darstellung von komplexen Mengen.
FRAGE: Das klingt alles sehr komplex. Wo fängt man denn da an?
DAMM: Wir haben einfach auf unsere Intuition gehört: Es kann ja kaum sein, dass wir auf der einen Seite in der Luftfahrtindustrie stetig fallende Unfallraten haben, es auf der anderen Seite aber diese Unentscheidbarkeitsresultate gibt. Also haben wir uns erstmal angeschaut, wie das die Fachleute in der Industrie machen. Wir arbeiten seit über 20 Jahren mit Airbus zusammen und kennen im Detail deren Entwicklungsprozesse. Dabei haben wir festgestellt, dass Welten liegen zwischen den Informatik-Theoretikern und der Industrie: Der Theoretiker will Situationen analysieren, die in der Praxis überhaupt nicht möglich sind – zum Beispiel, dass in einem endlichen Zeitintervall unübersehbare viele Informationen kodiert werden müssen. Der Blick in die Praxis zeigt aber, dass die Systeme getaktet sind, es passiert also gar nicht unbeschränkt viel. Das ist dann der Punkt, an dem wir Wissenschaftler tätig werden: Wir packen unsere Intuition in ein formales Modell. Das ist der Spaß des wissenschaftlichen Arbeitens.
FRAGE: Hat AVACS denn nun alle Probleme komplexer Systeme gelöst?
DAMM: Ich will es mal so sagen: Wir können aus AVACS heraus sagen, wie man Systeme bauen müsste, damit sie noch beherrschbar sind. Es ist ja so, dass die Systeme sich mittlerweile in Wechselwirkung befinden, ich sage nur das Schlagwort „Internet of things“: Jedes Teil hat einen eindeutigen Namen – egal ob Kaffeemaschine oder Fahrzeugersatzteil – alle sind einzeln ansprechbar im Netz. Das bringt der Industrie große Vorteile, die Logistik kann beispielsweise ihre Produktionsabläufe optimieren, weil alles beobachtbar ist. Die Marktdynamik ist allerdings derart stark, dass die Firmen rein pragmatisch anfangen, irgendetwas aufzubauen und dann wächst da ein System, das nicht mehr analysierbar ist. In der Logistik mag das ja noch gehen, bei sicherheitskritischen Systemen wie dem autonomen Fahren ist das schlichtweg inakzeptabel. Wir machen uns als Gesellschaft abhängig von ad-hoc gewachsenen Systemen, deren Risiken wir nicht mehr beherrschen.
FRAGE: Jetzt machen Sie mir irgendwie Angst...
DAMM: Naja, AVACS hat ja gezeigt, wie man die Systeme bauen müsste, damit sie beherrschbar bleiben. Und es gibt erste Erfolge: Die Kollegen in Saarbrücken sind stolz darauf, einen namhaften Halbleiterhersteller überzeugt zu haben, eine Prozessorgeneration so zu bauen, dass sie analysierbar ist.
FRAGE: AVACS ist ja nun offiziell beendet. Liegt der Abschlussbericht schon vor?
DAMM: Fast, wir liegen in den letzten Zügen.
FRAGE: Wie dick kann ich ihn mir vorstellen?
DAMM: Exakt 140 Seiten, das ist eine Vorgabe der Deutschen Forschungsgemeinschaft. Das ist schon eine Herausforderung, zwölf Jahre Forschung auf so wenigen Seiten abzubilden. Wir werden uns auf Highlights beschränken müssen. Aber diese 140 Seiten sind ja zum Glück nicht das einzige, was von AVACS bleibt. Es gibt viele Projekte, die sich anschließen. Hier an der Universität Oldenburg wollen wir in mehreren Folgeprojekten den Menschen in den Mittelpunkt stellen. Da passt es ganz gut, dass wir die Medizinische Fakultät vor Ort haben, wir arbeiten intensiv mit dem Department für Psychologie und dem Department für Versorgungsforschung zusammen. Wir wollen versuchen, den Menschen zu modellieren, dabei setzen wir insbesondere auf die Beobachtung der Gehirnaktivitäten.
FRAGE: Den Menschen modellieren? Das klingt jetzt irgendwie nach Science Fiction…
DAMM: Tatsächlich ist das gar nicht so abwegig. Das autonome Fahren wird schon bald Realität sein. Dabei spielt der Mensch trotzdem in bestimmten Situationen immer noch eine entscheidende Rolle. Stellen Sie sich vor, Sie sitzen in einem autonom fahrenden Auto, lehnen sich zurück und gucken einen Film. Plötzlich platzt ein Reifen und außerdem verliert der Lkw vor ihnen seine Ladung. Das Auto ist überfordert und sagt: Übernehmen Sie. Was brauchen Sie an dieser Stelle, um angemessen reagieren zu können? Was ist für uns als Menschen in so einer Extremsituation kognitiv überhaupt leistbar? Wir haben hier in Oldenburg eine fantastische Möglichkeit, gemeinsam mit den Kollegen der Medizin ein Stück weit in die Modellbildung des Menschen einzusteigen. Das ist Gegenstand des Projekts „Critical Systems Engineering for Socio-Technical Systems“, das sich aus AVACS ergeben hat. In diese Richtung planen wir übrigens auch einen neuen Sonderforschungsbereich. Wir wollen das nutzen, was wir in AVACS für technische Systeme entwickelt haben, um die Interaktion zwischen Mensch und technischem System zu verstehen.
FRAGE: Gibt es noch weitere Projekte?
DAMM: Da sind mehrere Transferprojekte, die die Brücke in die Industrie schlagen. Dabei geht es beispielsweise um das Verifizieren von Software in Assistenzsystemen. Mein Oldenburger Kollege Martin Fränzle hat Algorithmen entwickelt, die nun bei Airbus-Flugzeugen das Ausfahren der Räder sichern.
FRAGE: Also ziehen Sie ein durchweg positives Fazit…
DAMM: Definitiv. Es ist ein Forschungsfeld, was total begeisternd ist. Es ist relevant, es beinhaltet interdisziplinäres Arbeiten, man muss viel Mathematik können, es passt einfach alles super zusammen. Es ist alles andere als selbstverständlich gewesen, dass wir ein solches Teamdenken aufbauen konnten, dass über drei Standorte hinweg eine Wissenschaftler-Gemeinschaft entstanden ist. Es waren ja etwa 80 Forscher beteiligt. Und wir hatten eine ausgesprochen angenehme Arbeitsumgebung.
Interview: Birgit Bruns