A specification-based testing method of selection
| Autor: | Boin, Clément |
|---|---|
| Přispěvatelé: | Informatique, Biologie Intégrative et Systèmes Complexes (IBISC), Université d'Évry-Val-d'Essonne (UEVE)-Centre National de la Recherche Scientifique (CNRS), Université d'Evry-Val d'Essonne, Marc Aiguier(marc.aiguier@ibisc.univ-evry.fr), Davesne, Frédéric |
| Jazyk: | francouzština |
| Rok vydání: | 2007 |
| Předmět: |
tests à partir de spécifications
tests from specifications [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE] systèmes formels [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] tests selection criterion proof tree normlization spécifications algébriques formal systems normalisation d'arbres de preuves unfolding axioms critères de sélection de tests dépliage des axiomes algebraic specifications |
| Zdroj: | Génie logiciel [cs.SE]. Université d'Evry-Val d'Essonne, 2007. Français |
| Popis: | 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. 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|