HOL-TestGen

HOL-TestGen ist ein Test-Daten Generator für den spezifikationsbasierten Unit-Test. HOL-TestGen ist eine Erweiterung des interaktiven Theorembeweisers Isabelle/HOL.

hol-TestGen screenshot

HOL-TestGen erlaubt

das schreiben von Test Spezifikationen in Logik höherer Ordnung (HOL)
die Erzeugung von abstrakten Testfällen durch die (semi-) automatische Partitionierung des Eingaberaumes.
die automatische Auswahl von konkreten Testdaten
die automatische Generierung von Testskripten (in SML)
den Test von Implementierungen in verschiedenen Sprachen (z.B. C) durch den Einsatz eines foreign language interface.

HOL-TestGen ist freie Software und kann unter den Bedingungen einer BSD ähnlichen Lizenz weitergegebenwerden und wird von Achim D. Brucker und Burkhart Wolff entwickelt.

Download

hol-testgen-1.4.0.tar.gz (ca. 504 kByte, MD5: 5cc9c04b5e829fa729ec4c2a5fccb2fd, 2008-06-19) ChangeLog

Debian Pakete

Anwender von Debian GNU/Linux können HOL-TestGen auch aus folgender apt Quelle beziehen:

deb http://projects.brucker.ch/debian/rep unstable main
deb-src http://projects.brucker.ch/debian/rep unstable main

Hinweis: Bitte ersetzen Sie unstable mit der Distribution, die Sie nutzen; also stable, testing, oder unstable.

Publikationen

2010

Achim D. Brucker und Lukas Brügger und Paul Kearney und Burkhart Wolff. Verified Firewall Policy Transformations for Test-Case Generation. In International Conference on Software Testing, Verification, and Validation (ICST), 2010.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) ( )

2009

Achim D. Brucker und 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.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-642-00593-0_28) ( )

2008

Achim D. Brucker und Lukas Brügger und Burkhart Wolff. Verifying Test-Hypotheses: An Experiment in Test and Proof. In Electronic Notes in Theoretical Computer Science, 220 (1), pages 15-27, 2008. Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008)
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1016/j.entcs.2008.11.003) ( )
Achim D. Brucker und Lukas Brügger und Burkhart Wolff. Model-based Firewall Conformance Testing. In Testcom/FATES 2008. Lecture Notes in Computer Science (5047), pages 103-118, Springer-Verlag , 2008.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-540-68524-1_9) ( )

2007

Achim D. Brucker und Burkhart Wolff. Test-Sequence Generation with HOL-TestGen - With an Application to Firewall Testing. In TAP 2007: Tests And Proofs. Lecture Notes in Computer Science (4454), pages 149-168, Springer-Verlag , 2007.
Kategorien: , ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/978-3-540-73770-4_9) ( )

2005

Achim D. Brucker und Burkhart Wolff. HOL-TestGen 1.0.0 User Guide. ETH Zurich, Technical Report 482, 2005.
Kategorien: ,
(PDF) (BibTeX) (Endnote) (RIS) ( )
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.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/11759744_7) ( )

2004

Achim D. Brucker und Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. ETH Zurich, Technical Report 449, 2004.
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) ( )
Achim D. Brucker und Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Formal Approaches to Testing of Software. Lecture Notes in Computer Science (3395), pages 16-32, Springer-Verlag , 2004.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (doi:10.1007/b106767) ( )