Skip to Main content Skip to Navigation
New interface
Conference papers

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata
Contributor : Frédéric Dadeau Connect in order to contact the contributor
Submitted on : Friday, November 11, 2011 - 1:04:19 PM
Last modification on : Friday, January 21, 2022 - 3:08:57 AM

Links full text



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⟩



Record views