HOL-TestGen: An Interactive Test-case Generation Framework

Achim D. Brucker and Burkhart Wolff

We present HOL-TestGen, an extensible test environment for specification-based testing build upon the proof assistant Isabelle. HOL-TestGen leverages the semi-automated generation of test theorems (a form of a partition), and their refinement to concrete test data, as well as the automatic generation of a test driver for the execution and test result verification.

HOL-TestGen can also be understood as a unifying technical and conceptual framework for presenting and investigating the variety of unit and sequence 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. HOL-TestGen: An Interactive Test-case Generation Framework. In Fundamental Approaches to Software Engineering (FASE09). Lecture Notes in Computer Science (5503), pages 417-420, Springer-Verlag, 2009.
Keywords: symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
(PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-642-00593-0_28) ( )