Grey-Box Testing and Verification of Java/JML

Author

Dadeau, Frédéric ; Peureux, Fabien

Author_Institution

LIFC, Univ. de Franche-Comte, Besancon, France

fYear

2011

fDate

21-25 March 2011

Firstpage

298

Lastpage

303

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ICSTW.2011.30

Filename

5954423