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.7.1.tar.gz (ca. 5.3 MiB, MD5: 40df92dc26c2221ec0e92219f6356edd, 2012-11-19), unterstützt Isabelle 2011-1. ChangeLog

Ältere Versionen

• hol-testgen-1.6.0-pre.tar.gz (ca. 2.5 MiB, MD5: 0b089d97864d1084825b0c5452cb36f8, 2012-07-09), unterstützt Isabelle 2011.
• hol-testgen-1.5.0.tar.gz (ca. 1.9 MiB, MD5: 5dc5092fe94a3a2fb99b6733fbd1ba3b, 2010-10-04), unterstützt Isabelle 2009.

Publikationen

2013

• Achim D. Brucker, Lukas Brügger und Burkhart Wolff. HOL-TestGen/FW: An Environment for Specification-based Firewall Conformance Testing. In International Colloquium on Theoretical Aspects of Computing (ICTAC). Lecture Notes in Computer Science, Springer-Verlag , 2013.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi und Burkhart Wolff. Test Program Generation for a Microprocessor: A Case-Study. In TAP 2013: Tests And Proofs. Lecture Notes in Computer Science (7942), pages 76-95, Springer-Verlag , 2013.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2012

• Achim D. Brucker, Lukas Brügger, Matthias P. Krieger und Burkhart Wolff. HOL-TestGen 1.7.0 User Guide. Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, Technical Report 1551, 2012.
  Kategorien: ,
  (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Achim D. Brucker und Burkhart Wolff. On Theorem Prover-based Testing. In Formal Aspects of Computing, 2012.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s00165-012-0222-y) ( )
  
• Lukas Brügger. A Framework for Modelling and Testing of Security Policies. ETH Zurich,2012. ETH Dissertation No. 20513.
  (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Abderrahmane Feliachi. Semantics-Based Testing for Circus. Université Paris Sud,2012.
  (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Abderrahmane Feliachi, Marie-Claude Gaudel und Burkhart Wolff. Isabelle/Circus: A Process Specification and Verification Environment. In VSTTE.Lecture Notes in Computer Science, 7152, pages 243-260, 2012.
  (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-27705-4_20) ( )
  
• Abderrahmane Feliachi, Burkhart Wolff und Marie-Claude Gaudel. Isabelle/Circus. In Archive of Formal Proofs, 2012.
  (BibTeX) (Endnote) (RIS) (Word) (URL) ( )
  

2011

• Achim D. Brucker, Lukas Brügger, 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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1145/1998441.1998461) (ACM) ( )
  
• Matthias P. Krieger. Test Generation and Animation Based on Object-Oriented Specifications. University Paris-Sud XI,2011.
  (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  

2010

• Achim D. Brucker, Lukas Brügger, Matthias P. Krieger und Burkhart Wolff. HOL-TestGen 1.5.0 User Guide. ETH Zurich, Technical Report 670, 2010.
  Kategorien: ,
  (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• Achim D. Brucker, Lukas Brügger, 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, IEEE Computer Society , 2010.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1109/ICST.2010.50) ( )
  
• Achim D. Brucker, Matthias P. Krieger, 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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-00593-0_28) ( )
  

2008

• Achim D. Brucker, 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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1016/j.entcs.2008.11.003) ( )
  
• Achim D. Brucker, 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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (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: ,
  (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• 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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (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.
  Kategorien: ,
  (Zusammenfassung) (Artikel) (BibTeX) (Endnote) (RIS) (Word) ( )
  
• 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) (Artikel) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/b106767) ( )