I Overview
1 Describe, Analyze, Test
1.1 Model programs
1.2 Model-based analysis
1.3 Model-based testing
1.4 Model programs in the software process
1.5 Syllabus
2 Why We Need Model-Based Testing
2.1 Client and server
2.2 Protocol
2.3 Sockets
2.4 Libraries
2.5 Applications
2.6 Unit testing
2.7 Some simple scenarios
2.8 A more complex scenario
2.9 Failures in the field
2.10 Failures explained
2.11 Lessons learned
2.12 Model-based testing reveals the defect
2.13 Exercises
3 Why We Need Model-Based Analysis
3.1 Reactive system
3.2 Implementation
3.3 Unit testing
3.4 Failures in simulation
3.5 Design defects
3.6 Reviews and inspections, static analysis
3.7 Model-based analysis reveals the design errors
3.8 Exercises
4 Further Reading
II Systems with Finite Models
5 Model Programs
5.1 States, actions, and behavior
5.2 Case study: user interface
5.3 Preliminary analysis
5.4 Coding the model program
5.5 Simulation
5.6 Case study: client/server
5.7 Case study: reactive program
5.8 Other languages and tools
5.9 Exercises
6 Exploring and Analyzing Finite Model
Programs
6.1 Finite state machines
6.2 Exploration
6.3 Analysis
6.4 Exercise
7 Structuring Model Programs with Features and
Composition
7.1 Scenario control
7.2 Features
7.3 Composition
7.4 Choosing among options for scenario control
7.5 Composition for analysis
7.6 Exercises
8 Testing Closed Systems
8.1 Offline test generation
8.2 Traces and terms
8.3 Test harness
8.4 Test execution
8.5 Limitations of offline testing
8.6 Exercises
9 Further Reading
III Systems with Complex State
10 Modeling Systems with Structured State
10.1 “Infinite” model programs
10.2 Types for model programs
10.3 Compound values
10.4 Case study: revision control system
10.5 Exercises
11 Analyzing Systems with Complex State
11.1 Explorable model programs
11.2 Pruning techniques
11.3 Sampling
11.4 Exercises
12 Testing Systems with Complex State
12.1 On-the-fly testing 1
12.2 Implementation, model and stepper
12.3 Strategies 1
12.4 Coverage-directed strategies
12.5 Advanced on-the-fly settings
12.6 Exercises
13 Further Reading
14 Compositional Modeling
14.1 Modeling protocol features
14.2 Motivating example: a client/server protocol
14.3 Properties of model program composition
14.4 Modeling techniques using composition and features
14.5 Exercise
15 Modeling Objects
15.1 Instance variables as field maps
15.2 Creating instances
15.3 Object IDs and composition
15.4 Harnessing considerations for objects
15.5 Abstract values and isomorphic states
15.6 Exercises
16 Reactive Systems
16.1 Observable actions
16.2 Nondeterminism
16.3 Asynchronous stepping
16.4 Partial explorability
16.5 Adaptive on-the-fly testing
16.6 Partially ordered runs
16.7 Exercises
17 Further Reading
V Appendices
A Modeling Library Reference
A.1 Attributes
A.2 Data types
A.3 Action terms
B Command Reference
B.1 Model program viewer, mpv
B.2 Offline test generator, otg
B.3 Conformance tester, ct
C Glossary
Bibliography
