Une approche intégrée pour la conception par contrat (vérification statique / dynamique et génération automatique de test)

Les méthodes formelles légères facilitent l'introduction des outils formels en autorisant une spécification partielle du logiciel. En l'occurrence la granularité des vérifications dépend de la quantité d'information spécifiée. La fusion de ces méthodes semi-formelles (en particulier de la conception par contrat) et du test logiciel conduit à la notion de test basé sur les modèles (MBT). Ainsi, la découverte d'un oracle et la production des données de test peut être automatisée. Dans la génération automatique de tests, il est important de considérer le critère de qualité des tests produits. Cette qualité dépend des différents modes de productions. Le mode offrant la meilleur qualité consiste à analyser finement la spécification à l'aide de techniques de satisfaction de contraintes. Afin d'améliorer la qualité du logiciel, nous proposons dans cette thèse une méthodologie complète reposant sur la conception par contrat et différentes vérifications (dynamique et statique). En particulier, la génération automatique de tests dont l'enjeu est de produire de véritables scénarios de test qui suivent le plus précisément possible les spécifications ainsi qu'une stratégie de test clairement définie. La mise en œuvre des outils repose en grande partie sur un moteur de résolution de contrainte offrant une architecture ouverte. Ainsi l'utilisateur peut intégrer des types complexes qui ne sont pas supportés initialement grâce à la notion de constructeur de type. Nous présentons notamment le support pour deux types complexes: les tableaux bornés et les chaînes de caractères.PARIS-BIUSJ-Mathématiques rech (751052111) / SudocSudocFranceF