ACISI GECCOO - Tâche 4 : Détection d'erreursAvancement au 20 janvier 2005Equipe : Techniques Formelles et à Contraintes (TFC) du Laboratoire d'Informatique de l'université de Franche-Comté (LIFC) L'objectif est de s'appuyer sur la technologie BZ-Testing-Tools développée au LIFC, et basée sur la résolution de contraintes ensemblistes, pour permettre la détection d'erreurs dans les programmes ou modèles écrits en Java Modeling Language (JML). Ainsi nous nous proposons de donner des moyens pour valider un modèle, c'est-à-dire s'assurer de la conformité de ce modèle vis-à-vis des besoins initiaux. C'est un processus complémentaire à la vérification, qui vise à s'assurer de la consistence du modèle, même si celui-ci peut admettre des comportements non désirés. Ce sont ces comportements non désirés que notre approche vise, entre autres, à détecter. IntroductionL'animation est à l'heure actuelle l'un des plus sûrs moyens pour valider une spécification. Il s'agit d'un procédé qui consiste à exécuter le modèle de manière semi-automatique, car il requiert l'expertise humaine pour faire le lien entre les descriptions informelles d'un cahier des charges. En revanche, les résultats sont produits de manière automatique par un prototype logiciel permettant l'évaluation du modèle. BZ-Testing-Tools [ABC+02] est un environnement logiciel qui permet l'animation et la génération de cas de tests au limites pour les notations formelles B, Z ou Statecharts. Cet outil repose sur un format intermédiaire qui fédère les différentes notations, et appelé BZP. La prise en compte de JML dans cet environnement passe par l'extension de ce format de manière à permettre l'expression de concepts objets. Cette extension est également motivée par l'intégration en parallèle des diagrammes de classes UML avec contraintes OCL. L'objectif est dans un premier temps la création d'un module d'animation de spécifications JML sur lequel vont s'appuyer différents traitement permettant l'obtention de résultats pour la suite de la tâche 4. RésultatsDurant la première partie du projet, nous nous sommes intéressés à l'expression des spécifications JML dans le format intermédiaire de l'environnement BZ-Testing-Tools, permettant d'exprimer et de mettre en place un système de contraintes lors de l'animation. BZP étant basé sur un format pré-/post-conditions, ainsi que sur une syntaxe très expressive basée sur B, l'expression d'un large sous-ensemble de JML en BZP a été réalisé de manière immédiate. Néanmoins, il a été nécessaire d'étendre ce format pour exprimer des concepts objets. Au final, l'expression des spécifications JML dans le format BZP se rapproche de l'expression de JML dans B tel que décrit dans [BDG05]. Un animateur de spécifications JML s'appuyant sur l'utilisation possible de valeurs contraintes a ainsi été développé. Cet animateur, nommé JML-Testing-Tools [BDLU05], permet à un utilisateur de créer des instances d'objets et d'invoquer des méthodes sur ces instances, en laissant la possibilité de ne pas préciser les valeurs des paramètres d'entrée. Dans ce cas, une valeur contrainte est créée, dont le domaine est calculé à partir du type du paramètre et des contraintes locales (pré- et postconditions) à la méthode considérée. Il est alors possible d'effectuer à n'importe quel moment une valuation qui permettra d'assigner à ces valeurs contraintes une ou plusieurs valeurs de leur domaine. De plus, la vérification de propriétés, tels que l'invariant, peut être effectuée à la volée et des contre-exemples atteignables sont ainsi exhibés dans le cas où la propriété est détectée comme étant fausse. PerspectivesLes perspectives à mi-parcours sont basées sur l'animation symbolique mise en place dans la première moitié du projet.
Bibliographie
|