Chapter 1 - The challenge
1.1 What do we mean by testing?
1.2 Whats is model-based testing?
1.3 A smart card example
1.4 Summary
1.5 Further reading
Chapter 2 - The pain and the gain
2.1 Classic testing processes
2.2 The model-based testing process
2.3 Models: Build or borrow?
2.4 Your maturity level
2.5 Hypothetical case: total testing experience hours
2.6 Model-based testing experience reports
2.7 Benefits of model-based testing
2.8 Limitations of model-based testing
2.9 Summary
2.10 Further reading
Chapter 3 - A model of your system
3.1 How to model your system
3.2 A case study
3.3 Transition-based models
3.4 Pre/post models in B
3.5 Summary
3.6 Further reading
Chapter 4 - Selecting your tests
4.1 Structural model coverage
4.2 Data Coverage criteria
4.3 Fault-based criteria
4.4 Requirements-based criteria
4.5 Explicit test case specifications
4.6 Statistical test generations methods
4.7 Combining test selection criteria
4.6 Summary
4.7 Further reading
Chapter 5 - Testing from finite state machines
5.1 Testing qui-donc with a simple FSM
5.2 EFSMs and the odelJUnit Library
5.3 Unit testing Zlive with EFSMs
5.4 Labeled transition systems models
5.5 Summary
5.6 Further reading
Chapter 6 - Testing from pre/post models
6.1 How to write pre/post models for testing
6.2 The system process scheduler example
6.3 The triangle example
6.4 Robustness testing from a pre/post model
6.5 Testing a char system with Spec Explorer
6.6 Summary
6.7 Further reading
Chapter 7 - Testing from UML transition-based models
7.1 UML modeling
7.2 Testing an eTheater with LTG/UML
7.3 Testing a protocol with Qtronic
7.4 Summary
7.5 Further reading
Chapter 8 - Making tests executable
8.1 Principles of test adaptation
8.2 Example : the eTheater system
8.3 Summary
8.4 Further reading
Chapter 9 - The GSM 11.11 case study
9.1 Overview of the GSM 11.11 Standard
9.2 Modeling GSM 11.11 in B
9.3 Validation and verification of the B model
9.4 Generating test with LTG/B
9.5 Generating executable scripts
9.6 Test execution
9.7 Summary
9.8 Further reading
Chapter 10 - The ATM case study
10.1 Overview of the ATM system
10.2 Modeling the ATM system in UML
10.3 Generating test cases
10.4 Generating Executable test scripts
10.5 Executing the test
10.6 Summary
10.7 Further reading
Chapter 11 - Putting it into practice
11.1 Prerequisites for model-based testing
11.2 Selecting a model-based testing approach
11.3 Peple, roles, and training
11.4 Model-based testing and the agile methods
11.5 Model-based testing and the unified process
11.6 Epilogue
Appendix A - Summary of B Abstract Machine Notation
Appendix B - Summary of Common OCL Constructs
Appendix C - Commercial Tools
Glossary
Bibliography
Index
