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
Ältere Versionen
- hol-testgen-1.9.0.tgz
(ca. 1.4MiB, MD5: 6b2e391d986fdc2a17975eb76ac01af8, signed with 0x580E02C0, 2017-07-19),
unterstützt Isabelle 2016.
ChangeLog
- hol-testgen-1.9.0-non-free.tgz
(ca. 15MiB, MD5: cf855e9446ffbc381964c336ef2ad442, signed with 0x580E02C0, 2017-07-19),
unterstützt Isabelle 2016.
ChangeLog. < /br>
Das non-free Archiv enthält eine Kopie von Z3 und weitere Add-ons die restriktiveren Lizenzen unterliegen.
- hol-testgen-1.8.0.tar.gz
(ca. 1.3MiB, MD5: 11b9e32e785b167b6d261d658fd9bb6f, signed with 0x580E02C0, 2016-04-23),
unterstützt Isabelle 2013-2.
ChangeLog
- hol-testgen-1.8.0-pre.tar.gz
(ca. 238 KiB, MD5: 9e600a1d88e684275a8f07e555c8a439, 2015-06-04),
unterstützt Isabelle 2013-2.
- hol-testgen-1.7.1.tar.gz
(ca. 5.3 MiB, MD5: 40df92dc26c2221ec0e92219f6356edd, 2012-11-19),
unterstützt Isabelle 2011-1.
- 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
-
Achim D. Brucker, Lukas Brügger, Abderrahmane Feliachi, Chantal Keller, Matthias P. Krieger, Delphine Longuet, Yakoub Nemouchi, Frédéric Tuong und Burkhart Wolff.
HOL-TestGen 1.8.0 User Guide. Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, Technical Report 1586, 2016.
Kategorien: ,
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Achim D. Brucker und Burkhart Wolff.
Monadic Sequence Testing and Explicit Test-Refinements.
In TAP 2016: Tests And Proofs. Lecture Notes in Computer Science (9762), Springer-Verlag , 2016.
Kategorien:
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-319-41135-4_2) ( )
-
Achim D. Brucker, Lukas Brügger und Burkhart Wolff.
Formal Firewall Conformance Testing: An Application of Test and Proof Techniques.
In Software Testing, Verification & Reliability (STVR), 25 (1), pages 34-71, 2015.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1002/stvr.1544) ( )
-
Achim D. Brucker, Oto Havle, Yakoub Nemouchi und Burkhart Wolff.
Testing the IPC Protocol for a Real-Time Operating System.
In Working Conference on Verified Software: Theories, Tools, and Experiments. Lecture Notes in Computer Science, Springer-Verlag , 2015.
Kategorien:
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-319-29613-5_3) ( )
-
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 (8049), pages 112-121, Springer-Verlag , 2013.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-39718-9_7) ( )
-
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 als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-38916-0_5) ( )
-
Achim D. Brucker und Burkhart Wolff.
On Theorem Prover-based Testing.
In Formal Aspects of Computing (FAC), 25 (5), pages 683-721, 2013.
Kategorien: ,
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/s00165-012-0222-y) ( )
-
Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel und Burkhart Wolff.
The Circus Testing Theory Revisited in Isabelle/HOL.
In ICFEM. Lecture Notes in Computer Science, 8144, pages 131-147, Springer, 2013.
(Zusammenfassung) (Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-41202-8_10) ( )
-
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 als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) ( )
-
Lukas Brügger.
A Framework for Modelling and Testing of Security Policies. ETH Zurich,2012. ETH Dissertation No. 20513.
(Artikel als PDF Datei) (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 als PDF Datei) (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) ( )
-
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 als PDF Datei) (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 als PDF Datei) (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 als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-21210-9_33) ( )
-
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 als PDF Datei) (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 als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-68524-1_9) ( )