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

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) ( )
  
• 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) (doi:10.1109/ICST.2010.50) ( )
  

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) ( )