Résumé:

Cet exposé présente une transposition à Full Lotos des concepts et de la terminologie developés antérieurement pour les spécifications algébriques a Orsay [1], c'est-à-dire : une notion de "jeu de test exhaustif" est derivée de la sémantique de la notation formelle et de la définition d'une implementation correcte ; puis un jeu de test fini est sélectionné par des "hypothèses de sélection", qui sont déterminées à partir de
   - connaissances sur le programme,
   - des critères de couverture de la spécification,
   - et enfin des considérations de coût.

On définit les jeux de test exhaustifs correspondant aux relations d'implementation "red" et "conf" de Lotos, les verdicts associés, et l'hypothèse minimal requise des implémentations sous test pour assurer que le test exhaustif est non biaisé (aucun programme correct n'est rejeté) et valide (seuls
des programmes corrects sont acceptés).
Après optimisation, le jeu de test exhaustif obtenu pour la relation conf s'avère coincider avec les "must tests" utilisés habituellement comme base pour la dérivation de tests à partir de spécifications en LOTOS [2].

Cette unification ouvre des perspectives intéressantes de stratégies de test prenant en compte simultanément les aspects types de données et les aspects comportementaux de Full Lotos.

Références:

[1] Gaudel M.-C., "Testing can be formal too", invited conference, TAPSOFT'95, Aarhus, May 1995, L. N. C. S. n°915, Springer-Verlag, pp. 82-96.

[2]Tretmans J., "A formal approach to conformance testing", PhD thesis, Universiteit Twente, December 1992.

[3] Gaudel M.-C et P.D. James, "Testing Agebraic Data Types and Processes: a unifying theory", to appear in Formal Aspects of Computing.