Die Laureaten

Copyright © Klaus Tschira Stiftung / Peter Badge

Joseph Sifakis

geboren am 26. Dezember 1946 in Heraklion, Kreta (Griechenland)

Turing Award (2007) „zusammen mit Edmund Clarke und E. Allen Emerson für ihre Rolle dabei, die Modellprüfung zu einer hocheffektiven Methode zur Verifikation werden zu lassen, die heute in der Hard- und Softwareindustrie breite Anwendung findet.”

Sifakis, ein gebürtiger Grieche, besitzt seit 1976 die französische Staatsbürgerschaft. Er studierte Elektrotechnik an der Nationalen Technischen Universität Athen und Informatik an der Universität Grenoble. 1974 erhielt er den Doktortitel in Informatik und 1979 das doctorat d’État an der Universität Grenoble. Er ist ein Professor am EPFL in Lausanne und der Leiter des Centre de Recherche Intégrative in Grenoble.

Joseph Sifakis forschte am CNRS in Grenoble und gründete dort 1993 das Verimag Laboratory. Verimag ist ein führendes Forschungslabor für kritische eingebettete Systeme. Am Institut wurde die grundlegende Theorie und Technologie für das SCADE-Werkzeug entwickelt, das von Airbus beim Design und der Bewertung ihrer kritischen Echtzeit-Systeme verwendet wurde und heute einen de-facto-Standard in der Luftfahrtbranche darstellt. Verimag arbeitet auch seit Jahren strategisch mit ST Microelectronics, der France Telecom R&D und Airbus zusammen, wodurch eine ganze Reihe von Resultaten zu Validierung und Test in die Wirtschaft übertragen wurden.

Joseph Sifakis ist Mitglied der französischen Akademie der Wissenschaften, Mitglied der französischen National-Akademie der Ingenieure und Mitglied der Academia Europaea. Er ist Großoffizier der französischen Ehrenlegion. 2009 erhielt er die Leonardo-da-Vinci-Medaille.

Sifakis’ Arbeit ist gekennzeichnet durch ein immer wiederkehrendes Muster: das Problem wird zunächst von einem abstrakten, grundlegenden Blickwinkel aus untersucht; dies führt zu Methoden und Techniken für dessen Lösung. So gelangt man zu einer effektiven Implementierung, die erfolgreich in verschiedensten industriellen Anwendungen verwendet wird.

Von 1974 bis 1977 studierte Sifakis Petri-Netze und fand neue und grundlegende Ergebnisse für deren Verifikation und Leistungsbewertung. Von 1977 bis 1982 fokussierte er seine Arbeit mehr auf die Überprüfung von Übergangs-Systemen und entwickelte neue Resultate für die algorithmische Verifikation nebenläufiger Systeme, basierend auf einer Fixpunkt-Charakterisierung der Modalitäten einer in der Zeit verzweigten temporalen Logik. Diese Ergebnisse bildeten die Basis der Modellprüfung – der am weitesten verbreiteten Verifizierungs-Methode in der Industrie – und wurden erstmals im Modelprüfer CESAR umgesetzt. Diese Arbeit wurde in den Jahren 1982-1988 erweitert, um Modellprüfung und temporale Logik bei der Beschreibung der Spezifikationen nebenläufiger Systeme einzusetzen.

Im Zeitraum 1988-2000 dehnte Sifakis diese Arbeit aus, um Echtzeit-Systeme zu modellieren und zu verifizieren. Zu seinen wichtigsten Beiträgen gehören: 1) die Modellierung und Verifikation hybrider Systeme, also Modelle, die diskrete und kontinuierliche Dynamik kombinieren, 2) die Entwicklung und Umsetzung des KRONOS Modellprüfers, des ersten symbolischen Modellprüfers für zeitgesteuerte Automaten sowie 3) die Untersuchung symbolischer Synthese-Algorithmen für zeitgesteuerte Automaten.

Ab 1998 hat Sifakis aktiv das Aufkommen eingebetteter Systeme gefördert und trug zum Aufbau einer internationalen und lebendigen Forschungsgemeinschaft auf diesem Gebiet bei. Für mehr als zehn Jahre war er der wissenschaftliche Koordinator des European Network of Excellence on Embedded System Design ARTIST. Er war aktiv beteiligt am Aufbau von ARTEMISIA, des Industrieverbandes für eingebettete Systeme in Europa und ist einer der Mitbegründer der EmSoft Conference and Embedded Systems Week.

In dieser späteren Phase lag der Schwerpunkt von Sifakis’ Arbeit darin, das System-Design als einen Prozess zu formalisieren, der von konkreten Anforderungen hin zu Implementierungen führt, die verlässlich, optimal und bereits per Konstruktion korrekt sind. Seine Ergebnisse führten zur Entwicklung des BIP-Komponenten-Frameworks für strenges System-Design. Dieses Framework besteht aus einer Sprache und einem Satz von Werkzeugen, darunter dem Source-to-Source-Transformer, einem Compiler und dem D-Finder-Tool für kompositionale Verifikationstechnik. BIP ist einzigartig in seiner Mächtigkeit. Es kann gemischte Hard- und Software-Systeme beschreiben und verwendet einen kleinen und leistungsfähigen Satz von Primitiven für ein allgemeines Konzept für die Systemarchitektur. BIP wurde erfolgreich in mehreren industriellen Projekten eingesetzt, insbesondere bei der Komponentisierung von Legacy-Software und der automatischen Generierung von Implementierungen für Manycore-Plattformen.