A Precise Specification Framework for White Box Program Testing
Andreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith · TUbilio (Technical University of Darmstadt) · 2009
Coverage criteria for white box testing naturally fall into two groups: The first group are generic off-the-shelf criteria such as basic block coverage and condition coverage which are applied in the same uniform way to different source code. Although generic criteria are supported by industrial strength tools, simple experiments reveal that the tools disagree on standard notions such as condition coverage. The second group are code specific coverage criteria which are either defined on the fly during program development, or consciously designed to reflect requirements specific to the application and architecture. For the second group, there is a notable lack of tool support. In this paper, we aim to solve the problems of both groups – lack of precision and lack of adequate tool support – in a unified framework: We describe a specification language which designates coverage targets in the source code as building blocks for formal coverage criteria. On the one hand, our language FQL facilitates the precise specification of coverage criteria on the basis of a clean and intuitive semantics; on the other hand, we show how to apply the query-driven program testing paradigm presented at VMCAI 2009 for efficient test case generation with the help of a model checker. Experimental results demonstrate the practical feasibility of our framework.