Research
[Research] [Academic CV] [Publications] [Research Talks] [Teaching]
Publications
[sorted by type] [sorted by year] [sorted by topic]
pdfreaders.org

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
Categories: ,
Documents: (article)

QR Code for brucker.ea:interactive:2005.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
(article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/11759744_7) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@InCollection{ brucker.ea:interactive:2005,
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.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Formal Approaches to Testing of Software},
doi = {10.1007/11759744_7},
editor = {Wolfgang Grieskamp and Carsten Weise},
isbn = {3-540-25109-X},
keywords = {symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing},
language = {USenglish},
location = {Edinburgh},
number = {3997},
pdf = {http://www.brucker.ch/bibliography/download/2005/brucker.ea-interactive-2005.pdf},
project = {CSFMDOS},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Interactive Testing using {HOL}-{TestGen}},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-interactive-2005},
year = {2005},
}