ACISI GECCOO - Tâche 4 : Détection d'erreurs

Avancement au 20 janvier 2005


Equipe : 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.


Introduction

L'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ésultats

Durant 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.


Perspectives

Les perspectives à mi-parcours sont basées sur l'animation symbolique mise en place dans la première moitié du projet.

  • Notre premier objectif est d'analyser les invariants et les pré- et postconditions pour permettre d'exhiber des résultats sur l'évaluation de la spécification (invariant trop fort, pré-conditions trop faibles, etc.). Par un mécanisme d'animation symbolique à contrainte, nous proposons d'analyser le modèle pour tenter de détecter d'éventuelles erreurs de modélisation, basant notre analyse soit sur les états du modèle, soit sur les transitions entre ces états.

  • L'exploitation des résultats de la preuve est également envisagée dans un second temps. En reprenant les obligations de preuve non prouvées et en considérant leur négation comme objectif de test, il deviendra possible d'exhiber un chemin d'exécution menant à l'inconsistence et par conséquent, un contre-exemple pourra être présenté.

  • Finalement, nous envisageons d'adapter la technologie de génération de cas de tests aux limites de BZ-Testing-Tools dans le cadre de JML, en utilisant les spécifications JML et en s'appuyant (ou non) sur le code Java correspondant.


Bibliographie

[ABC+02]
F. Ambert, F. Bouquet, S. Chemin, S. Guenaud, B. Legeard, F. Peureux, N. Vacelet and M. Utting. BZ-TT: A Tool-Set for Test Generation from Z and B using Constraint Logic Programming. In Proceedings of the CONCUR'02 Workshop on Formal Approaches to Testing of Software (FATES'02), August 2002.
[BDG05]
F. Bouquet, F. Dadeau and J. Groslambert. Checking JML Specifications with B Machines. In Proceedings of International Conference on Formal Specifications and Development in Z and B (ZB'05), April 2005.
[BDLU05]
F. Bouquet, F. Dadeau, B. Legeard and M. Utting. JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In Proceedings of 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Tool session (TACAS'05), April 2005.