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

Supplementary material:
[ Slides  ]

Please cite this work as follows:
A. D. Brucker and B. Wolff, “HOL-TestGen: An interactive test-case generation framework,” in Fundamental approaches to software engineering (FASE09), M. Chechik and M. Wirsing, Eds. Heidelberg: Springer-Verlag, 2009, pp. 417–420. doi: 10.1007/978-3-642-00593-0_28. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-testgen-2009/

BibTeX
@InCollection{ brucker.ea:hol-testgen:2009,
  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.},
  keywords  = {Symbolic Test Case Generations, Black Box Testing, White Box
               Testing, Theorem Proving, Interactive Testing},
  location  = {York, UK},
  author    = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Fundamental Approaches to Software Engineering {(FASE09)}},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {5503},
  doi       = {10.1007/978-3-642-00593-0_28},
  pages     = {417--420},
  editor    = {Marsha Chechik and Martin Wirsing},
  title     = {{HOL-TestGen}: An Interactive Test-case Generation
               Framework},
  areas     = {formal methods, software},
  year      = {2009},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-hol-testgen-2009/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-hol-testgen-2009/brucker.ea-hol-testgen-2009.pdf},
}