Return to search

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.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00419730
Date09 July 2007
CreatorsBoin, Clément
PublisherUniversité d'Evry-Val d'Essonne
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0016 seconds