(The systems that are modeled need not be finite.)
Chapter 5 introduces the modeling library and explains how to write model programs.
Chapter 6 introduces our primary model-based analysis technique, exploration.
We introduce the analysis and visualization tool, mpv (Model Program Viewer), and
explain how it can reveal errors like those discussed in Chapter 3.
Chapter 7 introduces features and model composition, which are used to build
up complex model programs by combining simpler ones, to focus exploration and
12 Describe, Analyze, Test
testing on interesting scenarios, and to express temporal properties to check during
analysis.
Chapter 8 introduces model-based testing for closed systems (fully controllable
systems with no nondeterminism). We show how to generate test suites using the
tool otg (Offline Test Generator). We show how to write a test harness for the
implementation, and how to execute the generated test suites using our test runner
tool ct (Conformance Tester). We discuss test coverage.
Part III extends our methods to ???infinite??? models that cannot be analyzed exhaustively.
Chapter 10 describes modeling with data types that have ???infinite??? domains, such
as numbers and strings, and collection types, such as sets, bags, sequences, and
maps, which provide rich data structures.
Chapter 11 is about analyzing systems with complex state.
Pages:
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42