Prof. Daniel Kröning

This page is available in German only!

Formale Modellierung und Verifikationstools

Daniel Kröning studierte Informatik an der Universität Saarbrücken und promovierte auch dort. Anschliessend war er 3 Jahre lang als Postdoc an der Carnegie Mellon University in Pittsburgh tätig. Seit Juni 2004 ist der 30-jährige Assistenzprofessor für Informatik am Institut für Computersysteme an der ETH Zürich. Im Interview mit Katja Abrahams spricht Daniel Kröning über sein Forschungsgebiet, d.h. die formale Modellierung und Verifikation von Hardware- und Softwaresystemen, seine Aufgaben als Koordinator des Informatik-Kolloquiums sowie seine Auffassung von der Lehre.

Januar 2007

Welches ist Ihr Hauptgebiet in der Forschung?

Mein Hauptinteresse gilt der formalen Modellierung von komplizierten Systemen, das kann z.B. die Hardware und Software des Computers betreffen, aber auch Systeme im weiteren Sinne, etwa biologische Systeme, bei denen die Zellen eines Organismus’ interagieren. Daneben betreibe ich formale Verifikation, denn es geht mir nicht alleine darum, zu beschreiben, wie etwas funktioniert, sondern ich möchte auch belegen können, dass das System eine bestimmte Eigenschaft hat, z.B. dass der Computer nicht abstürzen wird. Meine Arbeit hat also zwei Komponenten, zum einen geht es um die mathematische Modellierung von komplexen Systemen. Zum anderen muss man auch in der Lage sein, ein Programm zu schreiben, das eine Systembeschreibung einliest, dann das System untersucht und dem Benutzer schliesslich ausgibt, ob das System die gewünschten Eigenschaften hat.

Woran arbeiten Sie gerade?

Mein gegenwärtiges Hauptziel ist es, Software mit Hilfe eines Editors mit schöner graphischer Oberfläche verifizieren zu können, in den man Code in einer Programmsprache, wie z.B. Eiffel, Java oder C eingibt. Der Editor soll nun in der Lage sein, die Programmierfehler rot anzustreichen. Das sieht in etwa aus wie die Rechtschreibehilfe von Word, geht aber weit darüber hinaus. Denn bei Betätigung der rechten Maustaste soll mir das Tool erklären, welchen Programmierfehler ich gemacht habe und wie ich ihn beheben kann.

Finden derartige Verifikationstools bereits konkrete Anwendung in der Industrie?

Insbesondere in der Hardwareindustrie kommen solche Programme, auch Model-Checker genannt, sehr oft zum Einsatz. Einige erinnern sich vielleicht noch an den Vorfall vor einigen Jahren, als Intel mit Milliardenaufwand Prozessoren aus bereits verkauften Computern ausbauen lassen musste, da diese falsch rechneten. Derartige Fehler kann man heute im Voraus mit automatischen Verifikationstools finden.

Bei Microsoft werden Model-Checker bereits zur Verifikation von Software verwendet, und zwar bei Gerätetreibern für Maus, Tastatur, oder Netzwerk. Auch für sehr sicherheitskritische Anwendungen, beispielsweise im Flugzeugbau oder im Militär, werden Model-Checker für Software schon heute in der industriellen Praxis eingesetzt, etwa für die Marsmissionen der NASA.

Welche Vorlesung halten Sie dieses Semester und was halten Sie persönlich für besonders wichtig in der Lehre?

Ein Vorteil der ETH ist sicherlich, dass die Bereitschaft da ist, aktuelle Forschungsergebnisse mit in die Vorlesungen einfliessen zu lassen und nicht nur die klassischen Grundlagenfächer zu unterrichten. Ich bin der Meinung, man begeistert Studierende am meisten, indem man auch Neues und Zukunftsweisendes lehrt. In diesem Semester unterrichte ich "Formal Verification" als Wahlfach für fortgeschrittene Studierende. Im Sommersemester 2007 werde ich wieder die Vorlesung "Digitaltechnik" für Studierende im 2. Semester anbieten. Bei dieser Vorlesung lege ich sehr grossen Wert darauf, die Kursteilnehmer, die ja meist noch wenig Erfahrung mit Prüfungssituationen an der ETH haben, optimal vorzubereiten. Ich gebe ihnen Beispiele, wie Prüfungsaufgaben aussehen könnten und Tipps, wie sie sich am besten die Zeit einteilen. Auch ein Ausblick auf die spätere Anwendung des Gelernten in der Praxis ist mir sehr wichtig.

Sie betreuen dieses Jahr zum zweiten Mal das Informatik-Kolloquium. Was für Erfahrungen haben Sie damit gemacht?

Ich empfinde es als sehr interessante Aufgabe, das Kolloquium zu betreuen, da es mir die Gelegenheit gibt, renommierte Wissenschaftler aus aller Welt als Vortragende einzuladen. Dadurch, dass ich die Veranstaltung organisiere, habe ich viel persönlichen Kontakt mit den Gästen: Die Teilnahme an den Vorträgen und der anschliessende Apéro bieten ermöglichen es, sich mit internationalen Fachleuten auszutauschen, das hat man nicht alle Tage! Eine gewisse Herausforderung ist es, die Experten dazu zu bringen, ihre Vorträge so zu gestalten, dass sie der Allgemeinheit, d.h. auch Studierenden und Professoren, die sich auf andere Fachgebiete spezialisiert haben, zugänglich sind.

Warum soll man Informatik studieren?

Informatik sollte man studieren, da es meiner Meinung nach die Wissenschaft ist, die einem das breiteste Spektrum eröffnet, sowohl im Bereich der praktischen Anwendung als auch der theoretischen Ideen, die dahinter stehen. Alle anderen Wissenschaften sind für mich in diesem Sinne ein Kompromiss. Wenn es um sehr anwendungsorientierte Wissenschaften geht, wie z.B. die Elektrotechnik, wird wohl jeder den praktischen Bezug daran sehr schätzen, aber der eine oder andere wird möglicherweise die theoretische Tiefe etwas vermissen. Andererseits wird sich jemand, der ein sehr theoretisches Studium gewählt hat, manchmal fragen, was er damit im Berufsleben einmal anfangen soll. Das kann einem in der Informatik beides nicht passieren. Ausserdem ist es in der Informatik möglich, sich ganz nach Geschmack verschiedenen Teilgebieten zuzuwenden, ohne sich sofort festlegen zu müssen.

Ist Informatik oder ein Informatikstudium etwas Kreatives?

Das Schreiben, also das Erstellen von Literatur, gilt traditionell als kreativer Beruf. Informatiker dagegen haben, obwohl sie Programme und Spezifikationen schreiben, nicht denselben gesellschaftlichen Status. Dabei geht es in der Informatik genauso wie in der Kunst darum, etwas Neues zu schaffen und nicht nur darum, etwas bereits Existierendes zu beschreiben, wie es in anderen Wissenschaften oft der Fall ist. Von daher ist die Informatik für mich der Prototyp der kreativen Wissenschaft.

Haben Sie ein Schlusswort für unsere Studierenden?

Der Ratschlag, den ich Studienanfängern geben würde, ist, nie die Komplexität eines Programms zu unterschätzen. Je einfacher ein Programm aussieht, desto mehr Fehler hat es wahrscheinlich!