Interactive Testing using HOL-TestGen

By 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

Obsoleted by:
This publication has been obsoleted by the following publication:
A. D. Brucker and B. Wolff, “On theorem prover-based testing,” Formal Aspects of Computing (FAC), vol. 25, no. 5, pp. 683–721, 2013, doi: 10.1007/s00165-012-0222-y. Author copy: https://logicalhacking.com/publications/brucker.ea-theorem-prover-2012/

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Interactive testing using HOL-TestGen,” in Formal approaches to testing of software, W. Grieskamp and C. Weise, Eds. Heidelberg: Springer-Verlag, 2005. doi: 10.1007/11759744_7. Author copy: https://logicalhacking.com/publications/brucker.ea-interactive-2005/

BibTeX
@InCollection{ brucker.ea:interactive:2005,
  keywords    = {Symbolic Test Case Generations, Black Box Testing, White Box
                 Testing, Theorem Proving, Interactive Testing},
  abstract    = {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.},
  location    = {Edinburgh},
  author      = {Achim D. Brucker and Burkhart Wolff},
  booktitle   = {Formal Approaches to Testing of Software},
  language    = {USenglish},
  publisher   = {Springer-Verlag },
  address     = {Heidelberg },
  series      = {Lecture Notes in Computer Science },
  number      = {3997},
  doi         = {10.1007/11759744_7},
  isbn        = {3-540-25109-X},
  editor      = {Wolfgang Grieskamp and Carsten Weise},
  title       = {Interactive Testing using {HOL}-{TestGen}},
  areas       = {formal methods, software},
  year        = {2005},
  obsoletedby = {brucker.ea:theorem-prover:2012},
  note        = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-interactive-2005/}},
  pdf         = {https://logicalhacking.com/publications/brucker.ea-interactive-2005/brucker.ea-interactive-2005.pdf},
}