Achim D. Brucker und 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.

*Schlüsselwörter:* symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing

*Kategorien:* ,

*Dokumente:* (Artikel als PDF Datei)

Bitte zitieren sie diesen Artikel wie folgt:

Achim D. Brucker und Burkhart Wolff.
**Interactive Testing using HOL-TestGen**.
In *Formal Approaches to Testing of Software*. Lecture Notes in Computer Science (3997), Springer-Verlag, 2005.

*Schlüsselwörter:* symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing

(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/11759744_7) ( )

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}, | |

= | {https://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 | = | {https://www.brucker.ch/bibliography/abstract/brucker.ea-interactive-2005}, | |

year | = | {2005}, |