DigiCosme Tutorial "Model-based Testing"
The course will take place at Supelec, Amphi F3-05, 23.4.13, 9:00 - 12:30.
Many testing techniques vitally depend on symbolic computation and
constraint-solving techniques. Their limits therefore represent limits
for testing as a whole. The HOL-TestGen system is designed as plug-in into
the state-of-the-art theorem proving environment Isabelle/HOL. Thus, powerful
modeling languages as well as powerful automated and interactive proof methods
for constraint resolution are available. HOL-TestGen has been applied in unit,
sequence, and reactive sequence black-box test scenarios in substantial case
studies. Conceptually, it offers a quite unique combined view on these areas
traditionally considered separately. Moreover, it bridges the gap to traditional
program verification by concepts such as 'explicit test hypothesis'. The
tutorial is going to be a guided tour through theory, pragmatics, and
case-studies.
Downloads : Isabelle (Use Version 2011-1!) , HOL-TestGen
More from the HOL-TestGen Website.
Tutorial Material:
- Part I:
Instead of a Motivation: A Provocation,
A Gentle Introduction to Isabelle/HOL, Exercise 1 - Part II: The Blob. (Foundations, Advanced Scenarios, Applications) The HOL-TestGen Tutorial.
Downloads:
Downloads : Isabelle (Use Version 2011-1!) , HOL-TestGen
More from the HOL-TestGen Website.
Bibliography:
2013
-
Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff.
Test Program Generation for a Microprocessor: A Case-Study.
In TAP 2013: Tests And Proofs. Lecture Notes in Computer Science, Springer-Verlag , 2013.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) ( )
2012
-
Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff.
HOL-TestGen 1.7.0 User Guide. Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, Technical Report 1551, 2012.
Categories: ,
(article) (BibTeX) (Endnote) (RIS) (Word) ( ) -
Achim D. Brucker and Burkhart Wolff.
On Theorem Prover-based Testing.
In Formal Aspects of Computing, 2012.
Categories: ,
(abstract) (article) (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.
(article) (BibTeX) (Endnote) (RIS) (Word) ( ) -
Abderrahmane Feliachi.
Semantics-Based Testing for Circus. Université Paris Sud,2012.
(BibTeX) (Endnote) (RIS) (Word) ( ) -
Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff.
Isabelle/Circus: A Process Specification and Verification Environment.
In VSTTE.Lecture Notes in Computer Science, 7152, pages 243-260, 2012.
(article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-27705-4_20) ( ) -
Abderrahmane Feliachi, Burkhart Wolff, and 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, and 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.
Categories: ,
(abstract) (article) (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.
(article) (BibTeX) (Endnote) (RIS) (Word) ( )
2010
-
Achim D. Brucker, Lukas Brügger, Matthias P. Krieger, and Burkhart Wolff.
HOL-TestGen 1.5.0 User Guide. ETH Zurich, Technical Report 670, 2010.
Categories: ,
(article) (BibTeX) (Endnote) (RIS) (Word) ( ) -
Achim D. Brucker, Lukas Brügger, Paul Kearney, and 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.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1109/ICST.2010.50) ( ) -
Achim D. Brucker, Matthias P. Krieger, Delphine Longuet, and 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.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-21210-9_33) ( )
2009
-
Achim D. Brucker and 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.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-00593-0_28) ( )
2008
-
Achim D. Brucker, Lukas Brügger, and 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)
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1016/j.entcs.2008.11.003) ( ) -
Achim D. Brucker, Lukas Brügger, and Burkhart Wolff.
Model-based Firewall Conformance Testing.
In Testcom/FATES 2008. Lecture Notes in Computer Science (5047), pages 103-118, Springer-Verlag , 2008.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-68524-1_9) ( )
2007
-
Achim D. Brucker and 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.
Categories: , ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-73770-4_9) ( )
2005
-
Achim D. Brucker and Burkhart Wolff.
HOL-TestGen 1.0.0 User Guide. ETH Zurich, Technical Report 482, 2005.
Categories: ,
(article) (BibTeX) (Endnote) (RIS) (Word) ( ) -
Achim D. Brucker and Burkhart Wolff.
Interactive Testing using HOL-TestGen.
In Formal Approaches to Testing of Software. Lecture Notes in Computer Science (3997), Springer-Verlag , 2005.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/11759744_7) ( )
2004
-
Achim D. Brucker and Burkhart Wolff.
Symbolic Test Case Generation for Primitive Recursive Functions. ETH Zurich, Technical Report 449, 2004.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) ( ) -
Achim D. Brucker and 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.
Categories: ,
(abstract) (article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/b106767) ( )