Grey-Box Testing and Verification of Java/JML

Frédéric Dadeau 1, 2 Fabien Peureux 1
2 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 : We present in this paper the application of constraint solving techniques to the validation and automated test cases generation for Java programs, annotated with JML specifications. The Java/JML code is translated into a constraint representation based on a subset of the set-theory, which is well-suited for modelling object-oriented programs. Symbolic code execution techniques can then be applied to produce test cases, using classical structural test selection criteria, or to detect possible runtime errors, and non-conformances between the Java code and its embedded JML model.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-00640381
Contributor : Frédéric Dadeau <>
Submitted on : Friday, November 11, 2011 - 1:04:19 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Identifiers

Citation

Frédéric Dadeau, Fabien Peureux. Grey-Box Testing and Verification of Java/JML. 3rd International Workshop on Constraints in Software Testing Verification and Analysis, Mar 2011, Berlin, Germany. pp.298-303, ⟨10.1109/ICSTW.2011.30⟩. ⟨hal-00640381⟩

Share

Metrics

Record views

398