M2R Course: Test of IT Systems
("Test des Systèmes Informatiques")
All courses will take place at Salle Firtech, Bat. 490, 9:00 - 12:00.
The Material below is tentative !!!
Downloads : Isabelle (Use Version 2009, not 2009-1!) , HOL-TestGen
Exam : 5.3.2009 ???
Resume due: 5.3.2009 (submit electronically to ~wolff@lri.fr !)
The Material below is tentative !!!
- C1 10.12. [BW]: Course Primer, Introduction to Testing, A Gentle Introduction to Isabelle/HOL Exercise 1
- 17.12. : Shifted because strike and snow ...
- C2 7.1. [BW] : (Unit)-Tests based on Data Models, Exercise 2
- C3 14.1 [BW] : (Unit)-Tests based on Data Models, cont., Exercise 3
- C4 21.1. [BW] : Sequence-Tests with HOL-TestGen
- C5 28.1. [BW] : Testing Reactive Systems
- C6 4.2. [BW] : White-Box-Tests based on Symbolic Execution with HOL-TestGen
- C7 11.2. [BW] :Finite Sequence Testing with Hidden State
- C8 18.2. [BW] :IOTS-Testing and IO-Conformance
Downloads : Isabelle (Use Version 2009, not 2009-1!) , HOL-TestGen
Exam : 5.3.2009 ???
Resume due: 5.3.2009 (submit electronically to ~wolff@lri.fr !)
Bibliography:
- [1] Model-Checking oriented Program-Based Testing: Test Input Generation with Java PathFinder
- [2] Symbolic Execution oriented Program-Based Testing: JPF-SE: A Symbolic Execution Extension to Java PathFinder
- [3] Compositional Symbolic Execution oriented Program-Based Testing:Demand-Driven Compositional Symbolic Execution PEX System Description
- [4] Random-based Testing: Testing Monadic Code with QuickCheck, QuickCheck Tutorial
- [5] Unit-Sequence-Reactive Testing: Test-sequence generation with hol-testgen - with an application to firewall testing
- [6] Application: Firewall Testing, Model-based Firewall Conformance Testing
- [7] Symbolic IOCO : A Symbolic Framework for Model-Based Testing,Testing of Reactive Systems The IOCO testing theory
- [8] Tools :Tools for Test Case Generation
- [9] Testing Non-Determinism: Optimal Strategies For Testing Nondeterministic Systems
- [10] Large-Scale Industrial Application: Using Model-Based Testing for Quality Assurance of Protocol Documentation
- [11] Invariant Generation By Tests: From Tests To Proofs
- [12] Testing Pointer Programs : Test Input Generation for Programs with Pointers