Équipe TFC
rapport d'avancement final

LIFC, Besançon

Composition équipe TFC, LIFC, Besançon

[h] Bellegarde Françoise Professeur A quitté le projet en Janvier 2006
Bouquet Fabrice MCF (HDR) A soutenu son habilitation le 24 Juin 2005
Dadeau Frédéric Docteur A soutenu sa thèse le 19 Juillet 2006
  Allocation ministère liée à l'ACI A quitté le projet le 1 Octobre 2006
Giorgetti Alain MCF  
Groslambert Julien Doctorant (3ème année)  
  Allocation ministère  
Julliand Jacques Professeur  
Kouchnarenko Olga Professeur Professeur depuis le 1 septembre 2006
Legeard Bruno Professeur A quitté le projet en Février 2006
Masson Pierre-Alain MCF  

JML-Testing-Tools

Le premier travail que nous avons effectué dans le projet est de réaliser les extensions nécessaires à l'approche BZ-Testing-Tools pour prendre en compte les concepts de la notation JML.

Pour ce faire, nous sommes partis d'un environnement d'animation et de résolution de contraintes logico-ensembliste [6], initialement conçu pour la prise en compte de spécifications B, et basé sur un format intermédiaire nommé BZP. Nous avons proposé une représentation des états mémoire Java dans ce format ensembliste, permettant ainsi leur expression sous la forme de systèmes de contraintes. Nous avons ensuite défini l'expression de spécifications JML dans le format BZP, qui nous a permis de pratiquer l'animation de la spécification [8, 7].

L'utilisation de l'animation a permis de réaliser un premier travail sur la mise au point de spécification [4]. Nous avons aussi chercher à vérifier les spécifications JML en utilisant les outils du monde B en définissant les règles de traduction [1] et ensuite en réalisant un outil permettant d'effectuer cette traduction de façon automatique [2].

La dernière étape du travail concerne la génération de séquence de tests [9]. Nous avons étendu la notion de génération de tests aux limites pour les programmes Java à partir de leur spécification JML. Nous avons ainsi défini deux types d'objectifs de tests. Le premier concerne l'activation des comportements extraits des spécifications JML des méthodes [5]. La seconde concerne l'utilisation de propriétés de sécurité comme objectif de tests [3]. Nous avons défini différents critères de couverture à partir de la spécification. Nous avons à cette occasion défini la notion de "valeur aux limites" pour des objets.

Raffinement en JML de l'application Demoney

Au LIFC, une expérience a été menée pour spécifier par raffinement en JML l'application Demoney. L'expérience a consisté à adopter une démarche de « spécification pure », dans le sens où la spécification a été réalisée indépendamment de toute idée d'implantation, et à partir de la seule spécification publique de Demoney. Les objectifs de l'expérience étaient les suivants : Nous rappelons que l'intérêt d'adopter une démarche de spécification par raffinement en JML est double : Le modèle le plus abstrait, point de départ de la démarche de spécification par raffinement, a été simplement constitué par la liste des commandes de Demoney. Puis les détails de la spécification publique ont été introduits un à un, du plus intuitif au plus technique, chaque détail introduit donnant naissance à un nouveau modèle JML raffinant le précédent.

Au final, 13 niveaux de raffinement ont été développés, jusqu'à la spécification de la communication par APDU mise en oeuvre dans Demoney. La spécification a pu être réalisée en n'utilisant que des fonctionnalités courantes de JML, ce qui valide le fait qu'une telle démarche est aisément adoptable à grande échelle. L'expérience a également montré qu'une démarche démarche de spécification incrémentale est valide, dans le sens où il n'a pas été nécessaire de modifier a posteriori les niveaux abstraits au fur et à mesure de l'introduction de chacun des détails spécifiés.

La spécification de la communication par APDU (très technique) a provoqué un fort accroissement de la taille de la spécification, puisque le modèle est passé en une étape de 350 lignes à 900 lignes de code JML. A ce niveau de détail, la taille de la spécification devient comparable à celle d'une implémentation telle que celle de Trusted Logic, qui est constituée de 1300 lignes de code Java.

Le modèle a pu être validé et animé au moyen de l'outil JML-TT animator. La preuve de la correction du raffinement d'un niveau à l'autre nécessite encore un outil de génération des obligations de preuve du raffinement.

References

[1]
F. Bouquet, F. Dadeau, and J. Groslambert. Checking JML Specifications with B Machines. In Proceedings of the International Conference on Formal Specification and Development in Z and B (ZB'05), volume 3455 of LNCS, pages 435–454, Guildford, United Kingdom, April 2005. Springer-Verlag.

[2]
F. Bouquet, F. Dadeau, and J. Groslambert. JML2B: Checking JML specifications with B machines. In B'2007, the 7th Int. B Conference - Tool Session, volume 4355 of LNCS, pages 285–288, Besancon, France, January 2007. Springer. To appear.

[3]
F. Bouquet, F. Dadeau, J. Groslambert, and J. Julliand. Safety property driven test generation from JML specifications. In FATES/RV'06, 1st Int. Workshop on Formal Approaches to Testing and Runtime Verification, volume 4262 of LNCS, pages 225–239, Seattle, WA, USA, August 2006. Springer.

[4]
F. Bouquet, F. Dadeau, and B. Legeard. How symbolic animation can help designing an efficient formal model. In Procs of the 7th Int. Conf. on Formal Engineering Methods (ICFEM'05), volume 3785 of LNCS, pages 96–110, Manchester, UK, November 2005. Springer-Verlag.

[5]
F. Bouquet, F. Dadeau, and B. Legeard. Automated boundary test generation from JML specifications. In FM'06, 14th Int. Conf. on Formal Methods, volume 4085 of LNCS, pages 428–443, Hamilton, Canada, August 2006. Springer-Verlag.

[6]
F. Bouquet, F. Dadeau, and B. Legeard. JML-Testing-Tools, un animateur symbolique de spécifications JML. In AFADL'06, Approches Formelles dans l'Assistance au Développement de Logiciels, Paris, France, March 2006. Session outils.

[7]
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), volume 3440 of Lecture Notes in Computer Science, pages 551–556, Edinburgh, United Kingdom, April 2005. Springer-Verlag.

[8]
F. Bouquet, F. Dadeau, B. Legeard, and M. Utting. Symbolic Animation of JML Specifications. In Proceedings of the International Conference on Formal Methods (FM'2005), volume 3582 of Lecture Notes in Computer Science, pages 75–90, Newcastle Upon Tyne, United Kingdom, July 2005. Springer-Verlag.

[9]
F. Dadeau. Animation de modèles jml et génération de tests fonctionnels. In MAJECSTIC'06, MAnifestation de JEunes Chercheurs STIC, Lorient, France, November 2006.
This document was translated from LATEX by HEVEA.