Team manager

Thierry Jéron
tél : +33 2 99 84 74 64
thierry.jeron@inria.fr

Presentation

Reactive systems are often critical systems, as errors occuring during their execution may have dramatic economical or human consequences. The correctness of such systems is thus essential. This can be ensured either by formally verifying properties on specifications, or by testing the conformance of implementations with respect to their specifications, or by forbidding unexpected behaviors of implementations using controllers.

The aim of the project is to improve the reliability of reactive systems by providing software engineers with methods and tools for automating the test generation and controller synthesis from formal specifications. We develop formal models for objects and relations occurring in testing and control, and algorithms for automatic test and controller synthesis. We implement prototype tools for industrial transfer or distribution in the academic world.

Our research is based on verification techniques such as model-checking, theorem proving, static analysis, the control theory of discrete event systems, and their underlying models and logics. The close connection between testing and control produces a synergy between these themes and allows to share models, techniques and tools.

Our privileged application domains are telecommunication systems, embedded systems, smart-cards, and control-command systems.

Research themes

• Combining test generation and controller synthesis
• Enumerative and on-the-fly techniques
• Symbolic techniques
• Compositionality and distribution
• Optimality and quality

Miscs

• 2010 activity report
• 2009 activity report
• 2008 activity report
• 2007 activity report