VERTECS

Modèles et techniques de vérification appliqués au test et au contrôle de systèmes réactifs

Contexte et objectifs

Projet de l'IRISA commun avec l'INRIA, le CNRS, l'INSA de Rennes, l'université de Rennes 1

Les systèmes réactifs sont souvent des systèmes critiques, au sens où l'occurrence d'erreurs au cours de leur fonctionnement peut avoir des conséquences graves du point de vue économique ou de la sécurité des personnes. Leur correction est donc primordiale. Cette correction peut être envisagée par vérification des propriétés attendues sur une spécification, par contrôle en empêchant les comportements fautifs, ou par test de l'implémentation d'un tel système vis à vis d'une spécification.

L'objectif du projet est d'améliorer la fiabilité des systèmes réactifs et critiques en fournissant à l'ingénieur logiciel des méthodes et des outils permettant d'automatiser le plus possible la génération des test et la synthèse de contrôleurs à partir de spécifications formelles de tels systèmes. Les moyens mis en oeuvre sont la conception de modèles formels des objets et relations intervenant dans le test et le contrôle, la conception d'algorithmes de génération de tests et de synthèse de contrôleurs et leur prototypage en vue d'un transfert industriel ou d'une distribution dans le milieu académique.

Nous fondons nos recherches sur les techniques de vérification telles que le model-checking, la preuve, l'analyse statique, la théorie du contrôle des systèmes à événements discrets, et les modèles et logiques qui les sous- tendent. Ce cadre mathématique est le moyen d'assurer la pertinence et les propriétés essentielles de correction des tests et contrôleurs produits. La proximité des problématiques de la génération de tests et de la synthèse de contrôleurs nous permettent une synergie entre ces deux thèmes et une factorisation des modèles, techniques et outils.

Nos domaines d'application privilégiés sont les systèmes de télécommunication, les systèmes embarqués, les cartes à puces et les systèmes de contrôle commande.

Axes de recherche

• Interaction entre génération de tests et synthèse de contrôleurs
• Techniques énumératives et à la volée
• Techniques symboliques
• Compositionalité et répartition
• Optimalité et qualité

Relations internationales et industrielles

• Projet européen IST Agedis (IBM, Intrasoft, Imbus, FTR&D, Univ. Oxford, Verimag) sur la génération automatique et l'exécution de tests pour des composants logiciels répartis.
• Projet RNTL Cote (Softeam, FTR&D, et les projets Inria Triskell et Lande) sur le test, la vérification et la certification de composants logiciels.
• Action de développement AEE (Architectures Electroniques Embarquées avec PSA, Renault, Siemens, Sagem, Valeo, EADS) sur le test de systèmes embarqués dans l'automobile.
• Collaboration avec CP8-Schlumberger et le projet Inria Vasy sur la génération de tests symboliques pour des applications cartes à puces.
• Projet Castor (MATRA, TNI, AQL, CELAR) sur la conception d'architectures sécurisées d'un système d'information.
• Programme Van Gogh avec l'université de Twente (Pays-Bas) sur la génération de test.

Responsable scientifique

Thierry Jéron
+33 2 99 84 74 64
Secrétariat +33 2 99 84 25 77

À propos de l'équipe

Site web
Rapport d'activité

Thème

Logiciel et architectures

Les projets du même thème

Adresse

IRISA - Campus universitaire de Beaulieu - 35042 Rennes Cedex