Abstract FR:

Nous proposons une methode et un outil d'assistance a la selection de jeux de tests a partir de specifications algebriques. La methode consideree est une methode de test fonctionnel reposant uniquement sur la specification d'un logiciel. Chaque axiome d'une specification algebrique definit des proprietes des operations qui y apparaissent. L'objectif du test fonctionnel etant de montrer qu'un programme ne respecte pas certaines de ces proprietes, nous selectionnons des jeux de tests a partir des axiomes de la specification. Un test pour un axiome est une instance close de cet axiome. L'ensemble des instances closes d'un axiome est generalement infini. Il est donc necessaire de n'en considerer qu'un sous-ensemble fini. Cette restriction correspond a une hypothese de selection: on suppose que le succes du jeu de tests selectionne equivaut au succes du jeu de tests contenant toutes les instances de l'axiome. L'originalite de notre approche est que nous etablissons formellement ces hypotheses au prealable. Les jeux de tests correspondants sont ensuite selectionnes. Nous abordons egalement le probleme de l'existence d'une procedure de decision pour le succes des tests selectionnes. La methode de selection est definie a l'aide d'hypotheses de selections dont l'usage est donne en fonction de la structure de la specification et de la forme des axiomes. Pour chaque hypothese nous proposons une strategie de selection compatible. Nous nous interessons alors aux mecanismes permettant de mettre en uvre ces strategies. Nous definissons alors un outil d'assistance a la selection reposant sur des techniques issues de la programmation logique. La puissance de la methode et de l'outil est illustree sur des exemples pertinents. Enfin, nous donnons differentes voies de recherche ouvertes par les resultats de cette these