Skip to Main content Skip to Navigation
Conference papers

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 (UMR 6174), 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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Frédéric Dadeau <>
Submitted on : Monday, October 13, 2008 - 5:34:52 PM
Last modification on : Wednesday, September 16, 2020 - 10:43:01 AM



Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Marc Utting. JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'05, Apr 2005, Edinburgh, United Kingdom. pp.551-556, ⟨10.1007/b107194⟩. ⟨inria-00329995⟩



Record views