Une méthode de sélection de tests à partir de spécifications algébriques

Les travaux de cette thèse s'inscrivent dans le cadre de la vérification des logiciels et plus particulièrement du test à partir de spécifications algébriques. La soumission d'un jeu de tests exhaustif pour trouver toutes les erreurs d'un programme est généralement impossible. Il faut donc sélectionner un jeu de tests le plus judicieusement possible. Nous avons donc donné une méthode de sélection de tests par dépliage des axiomes de spécifications conditionnelles positives (clauses de Horn pour la logique équationnelle). Celle-ci permet de partitionner le jeu exhaustif des tests. Nous utilisons pour cela un critère de sélection qui utilise les axiomes de la spécification et qui peut être appliqué plusieurs fois de suite. Pour garantir de bonnes propriétés sur ce critère de sélection, nous avons également donné un cadre général pour la normalisation d'arbre de preuve. Il fonctionne pour n'importe quel système formel, et permet d'unifier un grand nombre de résultats en logique.This thesis deals with test data set selection from algebraic specifications. It is, most of the time, impossible to submit an exhaustive test set to find all the errors in a program. It is necessary to select a test set judiciously. Thus, we gave a method of test selection by unfolding axioms of a positive conditional specifications (Horn clauses for equational logic). This method allows to partition the exhaustive test set. We use for that a selection criterion which uses the axioms of the specification and which can be iterated several times. To guarantee good properties on this selection criterion, we also gave a framework for prof tree normalization. It works for any formal system, and permits to unify a great number of results in logic.EVRY-BU (912282101) / SudocSudocFranceF