JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP

Fabrice Bouquet 1 Frédéric Dadeau 1 Bruno Legeard 1 Marc Utting 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper describes a tool for symbolically animating JML specifications using Constraint Logic Programming. A customized solver handles constraints that represent the value of instance fields. We have extended a model-based approach to be able to handle object-oriented specifications. Our tool is also able to check properties during the simulation and exhibit counter-examples for false properties. Therefore, it can be used both for semi-automated verification and for validation purposes.
Type de document :
Communication dans un congrès
Nicolas Halbwachs and Lenore D. Zuck. International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'05, Apr 2005, Edinburgh, United Kingdom. Springer Berlin / Heidelberg, 3440, pp.551-556, 2005, Lecture Notes in Computer Science. 〈10.1007/b107194〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00329995
Contributeur : Frédéric Dadeau <>
Soumis le : lundi 13 octobre 2008 - 17:34:52
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00

Identifiants

Citation

Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Marc Utting. JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. Nicolas Halbwachs and Lenore D. Zuck. International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'05, Apr 2005, Edinburgh, United Kingdom. Springer Berlin / Heidelberg, 3440, pp.551-556, 2005, Lecture Notes in Computer Science. 〈10.1007/b107194〉. 〈inria-00329995〉

Partager

Métriques

Consultations de la notice

207