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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata
Contributor : Frédéric Dadeau Connect in order to contact the contributor
Submitted on : Monday, October 13, 2008 - 5:34:52 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 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