Interactive Testing using HOL-TestGen

Achim D. Brucker and Burkhart Wolff

HOL-TestGen is a test environment for specification-based unit testing build upon the proof assistant Isabelle/HOL@. While there is considerable skepticism with regard to interactive theorem provers in testing communities, we argue that they are a natural choice for (automated) symbolic computations underlying systematic tests. This holds in particular for the development on non-trivial formal test plans of complex software, where some parts of the overall activity require inherently guidance by a test engineer. In this paper, we present the underlying methods for both black box and white box testing in interactive unit test scenarios. HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit test techniques in a logically consistent way.

Keywords: symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
Categories: ,

Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Formal Approaches to Testing of Software. Lecture Notes in Computer Science (3997), Springer-Verlag, 2005.
Keywords: symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
(PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/11759744_7) ( )