formation par la recherche / formation doctorale / enseignement, stages / sujets de thèses

Méthodes symboliques pour la génération de tests de systèmes réactifs comportant des données

Localisation :Irisa, Rennes

Equipe Pampa

Responsable : Vlad RUSU (tél. direct : 02 99 84 75 17, email : Vlad.Rusu@irisa.fr)
Thierry JERON (tél. direct : 02 99 84 74 64, email : Thierry.Jeron@irisa.fr)

Mot-clés :système réactif, test boîte noire, spécification formelle, objectifs de test, génération de tests symboliques.

Sujet : Le test de conformité est un test de type boîte noire. On se donne une spécification d'un système, qui sert de modèle de référence, et une implémentation réelle de ce système (implementation under test ou IUT) dont on ne connait le comportement que par ses interactions avec l'environnement. Un test consiste à stimuler l'IUT par des événements, à observer les réactions de l'IUT, et à en déduire sa conformité ou non par rapport à la spécification. Le test de conformité permet de montrer la présence d'erreurs (non-conformité), mais ne permet pas en général de montrer leur absence (conformité). En pratique, les cas de test sont des programmes comportant des paramètres et des variables symboliques.

En nous basant sur notre expérience précédente avec l'outil de génération de tests TGV (qui repose sur des explorations énumératives de graphes d'états et produit des cas de test complètement instanciés), nous avons défini des modèles et proposé une approche pour générer des cas de test symboliques, qui sont corrects par construction. Cependant, les cas de test obtenus sont complexes en terme de nombre de variables et d'états: certaines variables sont redondantes, et certains états sont inaccessibles.

Le travail de thèse abordera ces problèmes. Il s'agit de définir et d'implémenter une véritable méthodologie de génération de tests symboliques, en combinant des techniques d'exploration de graphes, des techniques de propagation et de résolution de contraintes sur les variables symboliques et des techniques d'abstraction, pour produire des cas de test symboliques compatibles avec la demande industrielle.