Joseph Sifakis

Sifakis’ work is characterized by an unusual recurrent pattern: the problem is first studied from an abstract, foundational point of view, which leads to methods and techniques for its solution, which, in turn, leads to an effective implementation that is successfully used in multiple industrial applications. In what follows his main achievements are briefly presented from a historical perspective.

From 1974 to 1977 Sifakis studied Petri nets and other models for concurrent systems [1]. During this period Sifakis obtained original and fundamental results on the structural properties of Petri nets as well as on the performance evaluation of timed Petri nets. These results are extensively used today for scheduling data-flow systems.

From 1977 to 1982 he switched his attention to verification of transition systems. Once again his work yielded original results on the algorithmic verification of concurrent systems based on a fix-point characterization of the modalities of a branching time temporal logic. These results laid down the foundations of model checking – the most widely used verification method in industry – and have been implemented for the first time in the CESAR model checker [2].

This work was expanded during 1982-1988 to deal with model checking and temporal logics for the description of concurrent system specifications [3]. The development of the CESAR model checker was funded by France Telecom and was extensively used for the certification of communication protocols. He went on to development a theory and techniques for computing property-preserving abstractions, which  have been effectively used to verify complex systems.

In a later episode (1988-2000) he extended this work to deal with modeling and verification of real-time systems [7, 8, 9]. This included:

1. the study of hybrid models – models combining discrete and continuous dynamics;
2. the development and implementation of the KRONOS model checker, and, in collaboration with T. Henzinger, the first symbolic model checker for timed automata (work);
3. in collaboration with O. Maler and  A. Pnueli the development and implementation of an efficient symbolic synthesis algorithm for timed;
4. the study of compositional modeling techniques for real-time scheduling by using priorities.

In 1993 Sifakis founded the Verimag industrial laboratory, a joint-venture between the Computer Science and Applied Mathematics laboratory (IMAG) and VERILOG SA. Verimag has been funded by Airbus and Schneider Electric to develop methods and tools based on results produced by Sifakis and his team, mainly:

1. The SCADE synchronous programming environment based on the Lustre language, used by Airbus for more than 15 years to develop safety critical systems, a de facto standard for aeronautics. SCADE has been qualified as a development tool by the FAA, EASA, and Transport Canada under DO-178B up to Level A.
2. The ObjectGeode specification and validation tool for real-time distributed applications, which includes functional testing and verification techniques. This tool  was commercialized by Telelogic SA until the company was acquired  by IBM in 2008.

Since 1997, Verimag has been a public research laboratory, associated with CNRS and the University of Grenoble. It has played a prominent role in the area of embedded systems by producing cutting edge results and leading research initiatives and projects in Europe.

From 1998, Sifakis has actively promoted the emergence of embedded systems and has contributed to the constitution of an international and live research community in this area. He has been the Scientific Coordinator of the ARTIST European Network of Excellence on Embedded System Design which has coordinated research of leading European teams in embedded systems for more than 10 years. He actively contributed to setting up the ARTEMISIA industrial association for embedded systems in Europe and is a co-founder of the EmSoft Conference and Embedded Systems Week.

During this later period Sifakis has also played a major role in the development and implementation of the BIP component framework for rigorous system design [10,11]. The implementation consists of a language and a set of tools including source-to-source transformers, a compiler and the D-Finder tool for compositional verification. BIP is unique for its expressiveness [12,13]. It can describe mixed hardware/software systems. It uses a small and powerful set of primitives encompassing a general concept of system architecture. BIP was successfully used in several industrial projects, in particular for the componentization of legacy software and the automatic generation of implementations for many-core platforms.

Further information on Joseph Sifakis and his research can be found here.

Author: Cristian S. Calude