Supervision : Jacques MALENFANT

Co-supervision : PESCHANSKI Frédéric

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

La conception logicielle à base de composants consiste à développer des applications complexes par assemblage de briques de base réutilisables. Pour réduire les coûts engendrés par les erreurs éventuelles et/ou la quantité de tests devant être produits pour les dénicher, il faut intégrer de la sémantique dans les spécifications de composant. Les méthodes formelles légères facilitent l'introduction de cette caractérisation sémantique, en permettant notamment la spécification partielle du logiciel. La conception par contrat est l'exemple emblématique des méthodes semi-formelles de conception logiciel. L'intégration de la conception par contrat à la problématique du test logiciel conduit à la notion de test basé sur les modèles (MBT). L'objectif à terme concerne la génération automatisée, partielle ou totale, du processus de test (oracle, données de test, etc.) à partir du modèle. En raison du caractère partiel des spécifications, ils est important de considérer le critère de qualité des tests produits. Dans cette thèse, nous proposons une famille d'outils servant de cadre à la conception par contrat pour les composants logiciels. Au sein d'une même plateforme nous étudions à la fois la vérification dynamique et statique des contrats. Nous proposons également un puissant générateur de tests permettant de produire, de façon complètement automatisée, des scénarios de tests fidèles aux spécifications. Un moteur de résolution de contraintes se trouve au cœur de la plateforme, utilisé à la fois pour la vérification statique et la génération de test. La principale originalité de ce moteur CSP est de permettre, grâce à une architecture ouverte et particulièrement flexible, l'intégration de types complexes comme les types objet, les collections (tableaux, listes, etc.) ainsi que les chaînes de caractères. La génération de tests mettent en jeu des contraintes complexes sur les chaînes de caractères (notamment les contraintes sur les sous-chaînes et la comparaison), est l'une des contributions techniques de ce travail.

2007-2010 Publications