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

https://hal.inria.fr/inria-00329995
Contributor : Frédéric Dadeau <>
Submitted on : Monday, October 13, 2008 - 5:34:52 PM
Last modification on : Friday, July 6, 2018 - 3:06:09 PM

Identifiers

Citation

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⟩

Share

Metrics

Record views

273