Presentation / Exposé : Génération automatique de
tests de conformité: l'approche de TGV.
Séminaire Invité
LaMI, Université d'Evry, France, janvier 1999.
Slides
Thierry Jéron, Pampa/IRISA/INRIA.
Dans cet exposé, nous commencerons par situer le contexte du
test de conformité
des protocoles et le problème de la génération
des cas de test.
Ensuite, nous détaillerons l'approche adoptée dans notre
prototype TGV.
TGV est fondé sur une théorie du test dont le modèle
est une variante
des systèmes de transitions dans laquelle on distingue les événements
observables, les événements controlables et les événements
internes.
Cette théorie utilise une relation de conformité qui
permet d'identifier
formellement les implantations acceptables par rapport à une
spécification
et de raisonner sur la correction des tests.
La génération automatique de test dans TGV repose sur
la donnée d'une
spécification formelle (en SDL, Lotos, etc) et d'un objectif
de test
qui permet la sélection des cas de test.
L'algorithmique sous-jacente est dite "à la volée" au
sens où elle
évite la construction explicite du graphe de tous les comportements
de la spécification en guidant, d'une manière paresseuse,
la contruction
des comportements visés par l'objectif. Ces techniques issues
de la
vérification par modèle ou "model-checking" mettent en
oeuvre
des algorithmes de parcours de graphes adaptés à la génération
de test
et qui peuvent aussi être vus comme des diagnostics ou des explications
pour la vérification de certaines propriétés de
logique temporelle.