1 Reactive system 32
3.2 Implementation 34
3.3 Unit testing 41
3.4 Failures in simulation 44
3.5 Design defects 46
3.6 Reviews and inspections, static analysis 47
3.7 Model-based analysis reveals the design errors 47
3.8 Exercises 52
4 Further Reading 53
II Systems with Finite Models
5 Model Programs 57
5.1 States, actions, and behavior 57
5.2 Case study: user interface 59
5.3 Preliminary analysis 61
5.4 Coding the model program 64
Contents vii
5.5 Simulation 70
5.6 Case study: client/server 72
5.7 Case study: reactive program 82
5.8 Other languages and tools 92
5.9 Exercises 93
6 Exploring and Analyzing Finite Model
Programs 94
6.1 Finite state machines 94
6.2 Exploration 99
6.3 Analysis 106
6.4 Exercise 114
7 Structuring Model Programs with Features and
Composition 115
7.1 Scenario control 115
7.2 Features 117
7.3 Composition 121
7.4 Choosing among options for scenario control 129
7.5 Composition for analysis 131
7.6 Exercises 136
8 Testing Closed Systems 137
8.1 Offline test generation 137
8.2 Traces and terms 139
8.3 Test harness 142
8.4 Test execution 146
viii Contents
8.5 Limitations of offline testing 147
8.6 Exercises 148
9 Further Reading 150
III Systems with Complex State
10 Modeling Systems with Structured State 155
10.1 ???Infinite??? model programs 155
10.2 Types for model programs 157
10.3 Compound values 157
10.
Pages:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25