Research
Rigorous System Design
We study the design of mixed HW/SW systems as a formal iterative process involving steps leading from requirements to provably correct implementations. We require that design is model-based, component-based and accountable. Accountability means that it is possible to assert at any step which among the requirements are satisfied and which may not be satisfied.
The developed design methodology is supported by BIP theory and tools.
Recent research studies the design of Cyberphysical Systems as a sequence of property-preserving model transformations.
Component-based Construction - BIP
Objectives:We develop theory, methods and tools for building systems consisting of heterogeneous components. The focus is on the following challenging work directions:
- A framework for the incremental composition of heterogeneous components. Three different sources of heterogeneity are considered related to interaction, execution and abstraction.
- Correctness-by-construction for essential system properties such as mutual exclusion, deadlock-freedom and progress in order to minimize a posteriori validation.
- Automated support for component integration and generation of glue code meeting given requirements.
Theory on modelling real-time systems has been developed over the past ten years. It includes results on the expressiveness of existing coordination mechanisms as well as the development of the BIP framework. The BIP language allows the description of hierarchically structured component-based systems from atomic components by using two basic protocols (rendezvous and broadcast) and priorities. It supports a rigorous system design methodology where correctness is ensured by construction and by using property-preserving source-to-source transformations. A key idea is the extensive use of architectures as principles for organizing coordination so as to meet given characteristic properties. We have shown that architectures can be formalized in BIP as generic behavior transformers and have developed theory for their composition.
Applications of these results led to the development of the BIP (Behavior, Interaction, Priority) language and the associated tool chain. The chain allows the generation from a system model in the BIP language, a description (C++ code) executable on a dedicated platform. The BIP platform supports both single-threaded and multi-threaded execution as well as enumerative state space exploration and simulation. The generated state graphs can be analyzed by using IF-platform.
A description is available here.
Verification - Model Checking
The first results about property verification by evaluation of formulas are in my thesis (Thèse dEtat) 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.
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.
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.
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.
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.