Model-Based Testing over IOSTS enriched with function calls / Imen Boudhiba ; sous la direction de Pascale Le Gall

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Langue / Language : anglais / English

Catalogue Worldcat

Tests fonctionnels (informatique)

Programmation fonctionnelle (informatique)

Ingénierie des systèmes

Ingénierie dirigée par les modèles

Le Gall, Pascale (Directeur de thèse / thesis advisor)

Dague, Philippe (1951-....) (Président du jury de soutenance / praeses)

Poizat, Pascal (Rapporteur de la thèse / thesis reporter)

Salaün, Gwen (1977-....) (Rapporteur de la thèse / thesis reporter)

Gaston, Christophe (Membre du jury / opponent)

Prevosto, Virgile (Membre du jury / opponent)

Griffaton-Sonnet, Lucas (Membre du jury / opponent)

Université Paris-Saclay (2015-2019) (Organisme de soutenance / degree-grantor)

École doctorale Interfaces : matériaux, systèmes, usages (Palaiseau, Essonne ; 2015-....) (Ecole doctorale associée à la thèse / doctoral school)

Mathématiques et informatique pour la complexité et les systèmes (Gif-sur-Yvette, Essonne ; 2006-....) (Laboratoire associé à la thèse / thesis associated laboratory)

CentraleSupélec (2015-....) (Autre partenaire associé à la thèse / thesis associated third party)

Résumé / Abstract : Les systèmes réactifs sont modélisés avec différents types d'automates, tels que les systèmes de transitions symboliques à entrée sortie (IOSTS). L'exécution symbolique d'un IOSTS permet la génération de cas de test qui peuvent être exécutés sur une implantation concrète, afin de déterminer si elle est conforme à son modèle. Dans ce document, nous étendons les IOSTS avec des appels de fonctions utilisateur et analysons leur impact sur le système entier et viceversa. Cette thèse comble l'écart entre une approche basée sur le modèle où les fonctions utilisateur sont abstraites et une approche basée sur le code où les petits morceaux de code sont considérés séparément, indépendamment de la façon dont ils sont combinés. Selon le niveau de connaissance que nous avons sur ces fonctions, elles sont modélisées soit par une spécification complète, soit par une spécification partielle, soit juste comme des boîtes noires fournies sans aucune connaissance. Premièrement, lorsque les fonctions sont partiellement connues, nous utilisons des bouchons définis par des tables contenant des tuples représentatifs des données d'entrée/sortie. L'approche proposée emprunte au test "concolic", l'idée de mélanger l'exécution symbolique avec l'information obtenue à partir d'exécutions concrètes des fonctions (tables). Deuxièmement, si l'utilisateur est prêt à fournir d'autres spécifications, il serait intéressant d'utiliser des représentations plus complètes pour les fonctions. Par conséquent, nous proposons d'abstraire des comportements des fonctions par des contrats pré/post. Ensuite, nous étendons l'exécution symbolique en analysant les fonctions via leurs contrats. Enfin, lorsque les fonctions appelées sont complètement inconnues, nous présentons une approche pour extraire de nouveaux contrats pour eux en explorant les contraintes issues de l'exécution symbolique de l'IOSTS. De tels contrats reflètent les contraintes des fonctions qui rendent possible un certain comportement (exigence).

Résumé / Abstract : Reactive systems are modeled with various kinds of automata, such as Input Output Symbolic Transition Systems (IOSTS). Symbolic execution over an IOSTS allows test cases generation that can be executed on a concrete implementation, in order to determine whether it is conforming to its model. In this dissertation, we aim at extending the IOSTS framework with explicit user-defined function calls and analyze their impact on a whole system and vice-versa. The thesis bridges the gap between a model-based approach in which user-defined functions are abstracted away and a code-based approach in which small pieces of code are considered separately regardless of the way they are combined. According to the level of knowledge we have about these functions, they are modeled either by a complete specification, a partial specification, or even just as black-boxes provided without any knowledge. First, when functions are partially known, we use function stubs defined by tables containing representative input/output data tuples. The proposed approach borrows from concolic testing, the idea of mixing symbolic execution with information obtained from instrumented concrete executions (function tables). Second, if the user is willing to provide further specifications, it would be interesting to use more complete representations for called functions. Hence, we propose to abstract function behaviors by means of pre/post contracts. Then we extend symbolic execution by analyzing the functions through their contracts. Finally, when called functions are completely unknown, we present an approach to extract new contracts for them by exploring constraints coming from the IOSTS symbolic execution. Such contracts reflect constraints on the functions that make some behavior (requirement) feasible.