Test generation and animation based on object-oriented specifications

Génération de tests et animation à partir de spécifications orientées objet L'objectif de cette thèse est l'assistance à la génération de tests et à l'animation de spécifications orientées objet. Nous cherchons en particulier à profiter de l'état de l'art des techniques de résolution de satisfaisabilité en utilisant une représentation appropriée des données orientées objet. Alors que la génération automatique de cas de tests recherche un large ensemble de valeurs à fournir en entrée d'une application, l’animation de spécifications effectue les calculs qui sont conformes à une spécification à partir de valeurs fournies par l'utilisateur. L'animation est une technique importante pour la validation des spécifications.Comme fondement de ce travail, nous présentons des clarifications et une formalisation partielle du langage de spécification OCL (Object Constraint Language) ainsi que quelques extensions, afin de permettre la génération de tests et l'animation à partir de spécifications OCL.Pour la génération de tests, nous avons implémenté plusieurs améliorations à HOL-TestGen, outil basé sur le démonstrateur de théorème Isabelle, qui engendre des tests à partir de spécifications en Logique d’Ordre Supérieure (Higher-Order Logic ou HOL). Nous montrons comment des solveurs SMT peuvent être utilisés pour résoudre différents types de contraintes en HOL et nous présentons une approche modulaire de raisonnement par cas pour dériver des cas de tests. Cette dernière approche facilite l'introduction de règles de decomposition par cas qui sont adaptées aux spécifications orientées objet.Pour l'animation de spécifications, nous avons développé OCLexec, outil d'animation de spécifications en OCL. A partir de contrats de fonctions OCLexec produit les implémentations Java correspondantes qui appellent un solveur de contraintes SMT lors de leur exécution.