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, Lukas Brügger, Matthias Krieger und Burkhart Wolff entwickelt.

Download

hol-testgen-1.5.0-pre.tar.gz (ca. 1.9 MiB, MD5: 84409a44718ef6cd7e276ddeb33fa3b9, 2010-04-02) ChangeLog

Publikationen

2012

Achim D. Brucker und Burkhart Wolff. On Theorem Prover-based Testing. In Formal Aspects of Computing, 2012. To appear.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) ( )

2011

Achim D. Brucker und Lukas Brügger und Paul Kearney und Burkhart Wolff. An Approach to Modular and Testable Security Models of Real-world Health-care Applications. In ACM symposium on access control models and technologies (SACMAT)., pages 133-142, ACM Press, 2011.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1145/1998441.1998461) (ACM) ( )

2010

Achim D. Brucker und Lukas Brügger und Matthias P. Krieger und Burkhart Wolff. HOL-TestGen 1.5.0 User Guide. ETH Zurich, Technical Report 670, 2010.
Kategorien: ,
(PDF) (BibTeX) (Endnote) (RIS) (Word 2007) ( )
Achim D. Brucker und Lukas Brügger und Paul Kearney und Burkhart Wolff. Verified Firewall Policy Transformations for Test-Case Generation. In Third International Conference on Software Testing, Verification, and Validation (ICST), pages 345-354, 2010.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1109/ICST.2010.50) ( )
Achim D. Brucker und Matthias P. Krieger und Delphine Longuet und Burkhart Wolff. A Specification-based Test Case Generation Method for UML/OCL. In MoDELS Workshops. Lecture Notes in Computer Science (6627), pages 334-348, Springer-Verlag , 2010. Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling.
Kategorien: ,
(Zusammenfassung) (PDF) (BibTeX) (Endnote) (RIS) (Word 2007) (doi:10.1007/978-3-642-21210-9_33) ( )

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) (Word 2007) (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) (Word 2007) (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) (Word 2007) (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) (Word 2007) (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) (Word 2007) ( )
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) (Word 2007) (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) (Word 2007) ( )
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) (Word 2007) (doi:10.1007/b106767) ( )