Title :
Grey-Box Testing and Verification of Java/JML
Author :
Dadeau, Frédéric ; Peureux, Fabien
Author_Institution :
LIFC, Univ. de Franche-Comte, Besancon, France
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.
Keywords :
Java; constraint handling; formal specification; object-oriented programming; program testing; program verification; set theory; JML specification; JML verification; Java verification; automated test cases generation; constraint representation; constraint solving technique; embedded JML model; grey-box testing; object-oriented program modelling; runtime errors detection; set theory; structural test selection criteria; symbolic code execution technique; Arrays; Context; Contracts; Data models; Java; Object oriented modeling; Runtime; Java/JML; constraint solving; grey-box testing; set-theory; symbolic execution;
Conference_Titel :
Software Testing, Verification and Validation Workshops (ICSTW), 2011 IEEE Fourth International Conference on
Conference_Location :
Berlin
Print_ISBN :
978-1-4577-0019-4
Electronic_ISBN :
978-0-7695-4345-1
DOI :
10.1109/ICSTW.2011.30
