Design, Formalization and Analysis

The increasing complexity of critical systems, the need for reaching acceptable quality levels, the increase in productivity, require to improve the methods and tools of systems engineering. Formal description techniques (FDT), by their mathe ma tical foundations, the existence of automatic verification techniques (model-checking) and the availability of tools to carry these verifications, help to handle this complexity. FDT constitute the object of our research addressing formal models, the associated model-checking techniques and the tools supporting them.

Our goals are to increase the expressiveness of these formal techniques in particular concerning temporal aspects, the effectiveness of the associated model-checking algorithms and the integration of these formal techniques with the processes of systems engineering.

In this context, we investigate the models expressing parallelism, communication and temporal constraints and more precisely the modeling of the suspension/resumption mechanisms often met in the systems governed by preemptive scheduling. To analyze these models, we propose model-checking techniques (semi-algorithms and over-ap pro­xima tions for the models in which reachability is undecidable) and optimize them for scalability.

To validate our models and the associated model-checking algorithms, we develop the TINA toolbox (Time Petri Net Analyzer). TINA allows the edition, animation and formal verification of models described in Time Petri nets extended by external data, priorities and stopwatches.

To integrate our research results within the framework of systems engineering and to evaluate our tools, we participate to the Topcased project part of the French competivity cluster AE/SE - and to the ANR platform OpenEmbedd . In this context, we define the language FIACRE (Intermediate Form for Architectures of Embedded Distributed Components) in collaboration with project VASY /INRIA and the Acadie /IRIT team and we provide associated tools.

Our main research topics deal with:

  • integration of formal approaches into the user's processes,
  • formal techniques for description and verification of real time systems,
  • symbolic representation of state spaces for such systems,
  • reduction of combinatorial explosion,
  • parallelization of model-checking algorithms.

This work is supported by contractual projects. For more information on these research topics, projects or publications, refer to: