Procédures de recherche en génération de testes à partir de modèles de spécifications
Institution:
BesançonDisciplines:
Directors:
Abstract EN:
The works introduced in this thesis give operational research procedures in the context of automatic functional test generation from specification models. The operations of the model are transformed into graphs. The paths of these graphs represent the behaviors of the model. The constraint animation (i. E. The simulation of the execution) of the behaviors is performed by the set constraint solver CLPS-BZ. The main goal of the generation method is to produce a set of tests designed to cover a specific set of test targets. These targets are computed from the model behaviors and in accordance with coverage criteria. The most delicate part of a test generation is to find a path, called preamble, that allows to reach a test target from the initial state of the system. The part of the test called postamble resets the system in a state that allows to resume the test procedure and comes under a similar problem. This PhD thesis gives several procedures in order to generate the preamble and postamble. A breadth search algorithm based on the system behaviors is given for the preamble computation. Besides, several Best-First search procedures are evaluated in the context of forward and backward chaining animations to compute the preamble and postamble. These algorithms have been implemented and adapted to several notations of specifications: B and Statemate statecharts. These algorithms have been used on many industrial projects and are optimized to go large scale.
Abstract FR:
Les travaux présentés dans cette thèse proposent des procédures de recherche opérationnelle dans le cadre de la génération automatique de tests fonctionnels à partir de modèles de spécifications. Les opérations du modèle sont réécrites sous la forme de graphes. Les chemins de ces graphes représentent les comportements du modèle. L'animation contrainte -c'est-à-dire la simulation d'exécution- des comportements du modèle est réalisée au moyen du solveur logico-ensembliste CLPS-BZ. L'objectif général de la méthode de génération consiste à produire un ensemble de tests permettant de couvrir des cibles de test spécifiques. Ces cibles de test sont calculées à partir des comportements du modèle et en fonction de critères de couverture. La partie la plus délicate de la génération d'un test consiste à trouver un chemin, nommé préambule, permettant d'atteindre la cible de test à partir de l'état initial du système. La partie du test, nommée postambule, qui permet de réinitialiser le système pour enchaîner les tests, présente une problématique similaire. Cette thèse propose différentes procédures pour la génération du préambule et du postambule. Un algorithme en largeur se fondant sur les comportements du système est proposé pour le calcul du préambule. D'autre part, différents algorithmes de type best-first ont été évalués dans le cadre d'animation en chaînage avant et chaînage arrière. Les algorithmes proposés ont été implantés et adaptés pour différentes notations de spécifications : B et statechart Statemate. Ces algorithmes ont été mis en oeuvre sur plusieurs applications industrielles, et optimisés afin de permettre le passage à l'échelle.