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
Résumé : Les travaux présentés dans cette thèse proposent une méthode de génération automatique de tests à partir de modèles.Cette méthode emploie deux langages de modélisations UML4MBT et OCL4MBT qui ont été spécifiquement dérivées d'UML et OCL pour la génération de tests. Ainsi les comportements, la structure et l'état initial du système sont décrits au travers des diagrammes de classes, d'objets et d'états-transitions.Pour générer des tests, l'évolution du modèle est représente sous la forme d'un système de transitions. Ainsi la construction de tests est équivalente à la découverte de séquences de transitions qui relient l'état initial du système à des états validant les cibles de test.Ces séquences sont obtenues par la résolution de scénarios d'animations par des prouveurs SMT et solveurs CSP. Pour créer ces scénarios, des méta-modèles UML4MBT et CSP4MBT regroupant formules logiques et notions liées aux tests ont été établies pour chacun des outils. Afin d'optimiser les temps de générations, des stratégies ont été développé pour sélectionner et hiérarchiser les scénarios à résoudre. Ces stratégies s'appuient sur la parallélisation, les propriétés des solveurs et des prouveurs et les caractéristiques de nos encodages pour optimiser les performances. 5 stratégies emploient uniquement un prouveurs et 2 stratégies reposent sur une collaboration du prouveur avec un solveur.Finalement l’intérêt de cette nouvelle méthode à été validée sur des cas d'études grâce à l'implémentation réalisée.
Type de document :
Thèse
Génie logiciel [cs.SE]. Université de Franche-Comté, 2013. Français
Liste complète des métadonnées

Littérature citée [90 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01094360
Contributeur : Fabrice Bouquet <>
Soumis le : vendredi 12 décembre 2014 - 10:55:31
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : vendredi 13 mars 2015 - 10:35:48

Fichier

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

293

Téléchargements de fichiers

318