HOL-TestGen: An Interactive Test-case Generation Framework
by 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: ,
Documents: (article)
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
(article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-00593-0_28) (
| abstract | = | {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.}, | |
| address | = | {Heidelberg}, | |
| author | = | {Achim D. Brucker and Burkhart Wolff}, | |
| booktitle | = | {Fundamental Approaches to Software Engineering {(FASE09)}}, | |
| doi | = | {10.1007/978-3-642-00593-0_28}, | |
| editor | = | {Marsha Chechik and Martin Wirsing}, | |
| keywords | = | {symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing}, | |
| language | = | {USenglish}, | |
| location | = | {York, UK}, | |
| number | = | {5503}, | |
| pages | = | {417--420}, | |
| = | {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.pdf}, | ||
| publisher | = | {Springer-Verlag}, | |
| series | = | {Lecture Notes in Computer Science}, | |
| talk | = | {talk:brucker.ea:hol-testgen:2009}, | |
| title | = | {{HOL-TestGen}: An Interactive Test-case Generation Framework}, | |
| url | = | {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009}, | |
| year | = | {2009}, |