VERTECS Research team

Verification models and techniques applied to testing and control of reactive systems

Team 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

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

International and industrial relations

  • European IST project Agedis (IBM, Intrasoft, Imbus, FTR&D, Univ. Oxford, Verimag) on automated generation and execution of test suites for distributed component-based software.
  • RNTL French project Cote (Softeam, FTR&D, and Inria projects Triskell and Lande) on testing, verification and certification of software components.
  • AEE development initiative (On-Board Electronic Architecture with PSA, Renault, Siemens, Sagem, Valeo, EADS) on testing of embedded systems for automobiles.
  • Collaboration with CP8-Schlumberger and Vasy on symbolic test generation for smart-card applications.
  • Castor Project (with MATRA,AQL,TNI, CELAR) on the specification of secure software architectures.
  • VanGogh program with the university of Twente (The Netherlands) on test generation

Keywords: Verification models /testing Control of reactive systems

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social