White-box Testing by Combining Deduction-based Specification Extraction
and Black-box Testing
Bernhard Beckert and Christoph Gladisch
We propose to use deductive program verification systems to generate
specifications for given programs and to then use these specifications
as input for black-box testing tools. In this way, (1) the black-box
testing method can make use of information about the program's
structure that is contained in the specification, and (2) we get a
separation of concerns and a clear interface between program analysis
on the one hand and test-case generation and execution on the other
hand, which allows the combination of a wide range of tools.
The method for specification extraction using a program verification
calculus described in this paper has been successfully implemented in
the KeY program verification system.