Joseph Sifakis
Tel: (+33) 457 42 22 44


Model Checking and Verification of Transition Systems

First Results - 1982
The first results about “property verification by evaluation of formulas” are in my thesis (Thèse d’Etat) presented in June 1979. These results have been published in the paper “A Unified Approach for Studying the Properties of Transition Systems” - Theoretical Computer Science, Vol. 18, 1992. They include a fixpoint characterization of a simple logic with two modalities: possible and inevitable.

The results of my thesis have also been the basis for work with JP Queille which led to the development of the first model checker CESAR, in 1982. See the related publication. The tool allows translation of finite state CSP programs into Petri nets, extended with finite-valued variables. The verification method is symbolic, representing sets of model states as boolean expressions.
I also published a paper with JP Queille on “A Temporal Logic to Deal with Fairness in Transition Systems” in FOCS 1982, which uses a branching time temporal logic with an until operator to express fairness properties.

Tools for Model-checking and Testing1982-today
The above results are the basis for subsequent work with H. Garavel, S. Graf, JC Fernandez, L. Mounier and M. Bozga, for the development model checking tools for the verification of distributed systems, by enumerative techniques.
These led to three widely-distributed and -used verification environments:

  • CADP
    A tool for the construction and analysis of distributed processes developed by H. Garavel at INRIA.
    See the related publication.
  • IF toolbox
    A validation environment for component-based real-time systems, developed at Verimag.
  • TGV
    An automatic test case generator for communication protocols, integrated in the ObjectGeode tool commercialized by Telelogic.

Combining model-checking and model reduction techniques1984 -1991
I also investigated compatibility between equivalences induced by temporal logics and behavioral equivalences used in process calculi (the “Adequacy Problem” defined by R. Milner). This led to several journal papers. Some of these results are used for the combination of model reduction techniques and model checking techniques in CADP and IF.

Abstraction Techniques 1983-1994
In my paper on “Property Preserving Homomorphisms of Transition Systems”, presented at the workshop on "Logic of Programs", 1983, I was the first to study property-preserving abstraction techniques by relating model-checking and abstract interpretation founded by P&R Cousot. This work has been the starting point for collaborations with several researchers, including S. Graf, H. Saidi, and S. Bensalem. A comprehensive version of the theoretical results can be found here.

The results about using abstraction have been extended and successfully applied in the Inverst tool developed by S. Bensalem and Y. Lakhnech at Verimag. This work has also influenced other tools such as SAL, developed at SRI.

Timed and Hybrid Systems - 1991-1999
I developed, in collaboration with T. Henzinger, X. Nicollin and S. Yovine, the first symbolic model-checking algorithm for the verification of TCTL. This algorithm has been implemented in the Kronos tool at Verimag.
The Kronos tool has been extensively and successfully used for the verification of critical real-time systems for the PATH project by S. Tripakis and S. Yovine, in the framework of collaboration with UC Berkeley (1997-2001).

Kronos is, with UPAAL, one of the two existing widely used model checking tools for timed systems.

I also worked on the verification of hybrid systems, in collaboration with researchers from Verimag and R. Alur and T Henzinger.

These general results are complemented by work on the verification of specific classes of hybrid systems, in particular in collaboration with Amir Pnueli.

Finally, in collaboration O. Maler and A. Pnueli, I produced results on the synthesis of controllers for timed systems. These have been applied for schedulability analysis of real-time systems.