Action Spécifique no. 23 Techniques avancées de tests des systèmes complexes

Equipes participant à l'Action Spécifique
 
 

 

Equipes	Personnes impliquées
Irisa, projets Triskell et Vertecs	Claude Jard, Thierry Jéron, Yves Le Traon
LaBRI, équipe MVTsi (Modélisation, vérification et Test de systèmes informatisés)	Richard Castanet, David Janin
LAAS-CNRS, groupe Tolérance aux fautes et sûreté de fonctionnement informatique	Olfa Abdellatif-Kaddour, Jean Arlat, Hélène Waeselynck
LRI, équipe Programmation et Génie Logiciel	Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Gregory Lestiennes
VERIMAG, équipe Systèmes Asynchrones	Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon

Irisa, projets Triskell et Vertecs
Contact : Claude Jard

L'Irisa est un laboratoire de recherche publique regroupant 370 personnes dont 150 chercheurs ou enseignants chercheurs et 115 chercheurs en thèse. L'INRIA, le CNRS, l'Université de Rennes 1 et l'INSA de Rennes sont partenaires au sein de cette unité mixte de recherche. Les recherches de l'Irisa se développent au sein de vingt projets ou actions de recherche autour de quatre grands thèmes scientifiques : réseaux et systèmes - génie logiciel et calcul symbolique - interaction homme-machine, images, données, connaissances - simulation et optimisation de systèmes complexes.
Deux nouveaux projets du laboratoire souhaitent participer à cette action CNRS sur le test de robustesse. Il s'agit du projet Vertecs (animé par T. Jéron, chercheur Inria, 4 permanents) et du projet Triskell (animé par JM. Jézéquel, professeur, 5 permanents). C. Jard (DR CNRS) assurera la coordination.
Vertecs : Modèles et techniques de VÉRification appliquées au TEst et au Contrôle de Systèmes réactifs. L'objectif scientifique 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 de génération de tests et de synthèse de contrôleurs pour ce type de systèmes.
Triskell : Construction fiable et efficace d'applications par assemblage de composants logiciels. Le projet a pour objectif général la construction fiable et économiquement efficace d'applications par assemblage de composants logiciels décrits avec UML, en particulier dans le domaine des systèmes répartis et réactifs ayant des temps de réponse statistiquement contraints.
 
 

LaBRI (UMR 5800), équipe MVTsi (Modélisation, vérification et Test de systèmes informatisés)
Contact : Richard Castanet

L'activité de recherche sur le test au LaBRI s'exerce dans le cadre de l'équipe MVTsi (Modélisation, Vérification et test de systèmes informatisés). Cette recherche sur le test est active depuis plus de 15 ans. Elle est coordonnée par R. Castanet, professeur à l'ENSEIRB et chercheur au LaBRI. Les réseaux et protocoles de communication en sont le domaine d'application avec comme thèmes de recherche : la modélisation de protocoles de communications (automates étendus, automates à entrées-sorties, automates temporisés), les systèmes et architectures de test , le test de conformité et d'interopérabilité, la conjonction preuve et test, et surtout la génération automatique de séquences de test et leur couverture. Les activités actuelles sont centrées sur le test temporisé, la conjonction preuve-génération de tests et le test de systèmes mobiles. Cette activité a généré 5 publications dans des revues, 47 présentations dans des congrès, la participation à deux projets RNRT (Calife, Platonis) et 13 thèses.
 
 

LAAS-CNRS (UPR 8001), Groupe "Tolérance aux fautes et sûreté de fonctionnement informatique"
Contact : Hélène Waeselynck

Fondé en 1975 par Jean-Claude Laprie, le groupe "Tolérance aux fautes et sûreté de fonctionnement informatique", actuellement dirigé par David Powell, a une compétence reconnue dans le domaine de la sûreté de fonctionnement des systèmes informatiques, définie comme la propriété permettant aux utilisateurs d'un système de placer une confiance justifiée dans le service qu'il leur délivre. Les activités du groupe couvrent la prévention des fautes, la tolérance aux fautes, l'élimination des fautes et la prévision des fautes.
Les travaux relatifs à l'aspect élimination des fautes de conception ont notamment conduit à définir des méthodes et procédés de sélection probabiliste d'entrées de test, appliqués avec succès à des logiciels critiques fournis par des partenaires industriels. Contribuant à la fois aux aspects élimination et prévision des fautes, les travaux sur l'injection de fautes visent à la caractérisation de systèmes en présence de fautes et, plus généralement, à la validation de systèmes tolérant les fautes. Les efforts actuels intéressant directement l'Action Spécifique concernent le test ciblant la vérification de propriétés de sûreté, le test de logiciels orientés-objet, et la caractérisation des modes de défaillances de systèmes exécutifs (systèmes d'exploitation et middleware).
 
 

Laboratoire de Recherche en Informatique (LRI), équipe Programmation et Génie Logiciel
Contact : Marie-Claude Gaudel

Au sein du LRI et de l'équipe Programmation et Génie Logiciel, dirigée par Marie-Claude Gaudel, des résultats théoriques et pratiques importants ont été obtenus sur les spécifications formelles en général et plus spécifiquement sur le test de logiciel basé sur ces descriptions formelles.
Différents formalismes ont été étudiés pour servir de base à la sélection de jeux de test et à la détection d'erreur (problème de l'oracle) : Types Abstraits Algébriques, Lustre-SAGA, LOTOS complet, B. Deux outils ont été développés et expérimentés sur des études de cas industrielles : LOFT, pour les types abstraits algébriques, et Gatel, en collaboration avec le CEA pour Lustre-Saga. Ces outils sont essentiellement basés sur la résolution de contraintes.
Actuellement, un nouveau prototype est en développement. Il combine résolution de contraintes et génération aléatoire uniforme de structures combinatoires pour engendrer des jeux de test assurant une couverture équilibrée de certaines constructions du système (à spécifier selon l'objectif de test).
Depuis 1998, cette activité sur le test a donné lieu à 4 publications en revue, 2 communications en congrès internationaux avec actes, 5 présentations en workshop et 3 conférences invitées à des congrès internationaux.
Dans le cadre de cette action, on étudiera comment transposer les approches du test développées précédemment dans l'équipe pour sélectionner des fautes à injecter à partir de descriptions formelles de celles-ci. Pour ce faire, il sera éventuellement nécessaire d'aborder des modèles formels probabilistes.
 
 

VERIMAG, équipe "Systèmes Asynchrones"
Contact : Laurent Mounier

VERIMAG est une unité mixte de recherche du CNRS, de l'INPG, et de l'UJF (UMR 5104), dirigée par Joseph Sifakis, et membre de la fédération IMAG. Les activités de recherche menées dans ce laboratoire concernent les techniques formelles de conception et de validation de systèmes et logiciels critiques. VERIMAG a notamment une compétence reconnue dans ce domaine, autant sur le plan théorique que pour le développement d'outils de validation au niveau de l'état de l'art. Cet équilibre est maintenu en particulier grâce à un ensemble de collaborations et projets de recherche que le laboratoire entretient avec de nombreux partenaires académiques et industriels.
L'équipe "Systèmes Asynchrones", impliquée dans cette Action, s'intéresse plus spécifiquement aux applications de type protocoles de communication et systèmes repartis. Ses thèmes d'activité concernent la sémantique des langages de spécification pour les systèmes asynchrones, les techniques de validation basées sur le "model-checking", ainsi que les techniques d'abstraction permettant l'analyse des systèmes infinis. Cette équipe a notamment contribué à la réalisation de la boîte à outils Lotos CADP (avec l'INRIA/VASY), de l'outil de génération de tests de conformité TGV (avec l'IRISA/PAMPA), et de l'outil de calcul d'abstraction InVeSt (avec l'université de Kiel et le SRI). Elle développe actuellement un environnement de validation
pour les langages SDL et UML, basé sur une forme intermédiaire générique (IF) dédiée aux systèmes temps-réels asynchrones.