JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP - Archive ouverte HAL Access content directly
Conference Papers Year : 2005

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

(1) , (1) , (1) , (2)
1
2

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.

Dates and versions

inria-00329995 , version 1 (13-10-2008)

Identifiers

Cite

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⟩
151 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More