Article :
An experiment in automatic generation of test suites for protocols
with verification technology
Une expérience de génération automatique de suites de tests
pour les protocoles à l'aide de la technologie de la vérification
Version rapport de recherche de l'article à
paraître dans Science of Computer Programming,
Special Issue on Industrially Relevant Applications of Formal Analysis
Techniques, J. F. Groote and M. Rem editors,
Elsevier Science publisher
Fichier PostScript (171K)
Jean-Claude Fernandez, Spectre/Vérimag/Inria/Grenoble
Claude Jard. Pampa/IRISA/CNRS
Thierry Jéron. Pampa/IRISA/INRIA/Rennes
César Viho. Pampa/Irisa/Université/Rennes
Dans ce rapport nous décrivons une expérience de génération automatique
de suites de tests pour les protocoles.
Nous énonçons les résultats obtenus par la génération de suites de tests
fondée sur la technologie de la vérification appliquée à un protocol
industriel.
Dans cette expérience, plusieurs outils ont été utilisés:
l'outil commercial GEODE (VERILOG) a servi à la génération
du graphe d'état fini à partir de spécifications en LDS,
l'outil Aldebaran de l'a boîte à outil CADP a permis la minimisation
de systèmes de transitions,
et un prototype appelé TGV (pour {\em Test Generation using Verification
techniques}) et développé dans la boîte à outil CADP a permis
la génération de suites de tests.
TGV est fondé sur des techniques de vérifications telles que
le calcul de produit synchrone et la vérification à la volée.
Ces outils ont été appliqués à un protocole industriel, le DREX.
La comparaison des tests produits avec des tests écrits manuellement
montrent l'intérêt des techniques utilisées.