Stratégies de génération de tests à partir de modèles UML/OCL interprétés en logique du premier ordre et système de contraintes

Jérome Cantenot 1, 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This thesis describes an automatic test generation process from models.This process uses two modelling languages, UML4MBT and OCL4MBT, created specifically for tests generation. Theses languages are derived from UML and OCL. Therefore the behaviours, the structure and the initial state of the system are described by the class diagram, the object diagram and the state-chart.To generate tests, the evolution of the model is encoded with a transition system. Consequently, to construct a test is to find transition sequences that rely the initial state of the system to the states described by the test targets.The sequence are obtained by the resolution of animation scenarios. This resolution is executed by SMT provers and CSP solvers. To create the scenario, two dedicated meta-models, UML4MBT and CSP4MBT have been established. Theses meta-models associate first order logic formulas with the test notions. 7 strategies have been developed to improve the tests generation time. A strategy is responsible for the selection and the prioritization of the scenarios. A strategy is built upon the properties of the solvers and provers and the specification of our encoding process. Moreover the process can also be paralleled to get better performance. 5 strategies employ only a prover and 2 make the prover collaborate with a solver.Finally the interest of this process has been evaluated through a list of benchmark on various cases studies.
Document type :
Theses
Complete list of metadatas

Cited literature [90 references]  Display  Hide  Download

https://hal.inria.fr/tel-01094360
Contributor : Fabrice Bouquet <>
Submitted on : Friday, December 12, 2014 - 10:55:31 AM
Last modification on : Friday, May 17, 2019 - 11:39:52 AM
Long-term archiving on : Friday, March 13, 2015 - 10:35:48 AM

Identifiers

  • HAL Id : tel-01094360, version 1

Citation

Jérome Cantenot. Stratégies de génération de tests à partir de modèles UML/OCL interprétés en logique du premier ordre et système de contraintes. Génie logiciel [cs.SE]. Université de Franche-Comté, 2013. Français. ⟨tel-01094360⟩

Share

Metrics

Record views

336

Files downloads

418