4 Case study: revision control system 169
10.5 Exercises 181
11 Analyzing Systems with Complex State 183
11.1 Explorable model programs 183
11.2 Pruning techniques 186
11.3 Sampling 190
11.4 Exercises 190
12 Testing Systems with Complex State 191
12.1 On-the-fly testing 192
12.2 Implementation, model and stepper 194
12.3 Strategies 199
12.4 Coverage-directed strategies 203
12.5 Advanced on-the-fly settings 210
12.6 Exercises 218
13 Further Reading 219
Contents ix
IV Advanced Topics
14 Compositional Modeling 223
14.1 Modeling protocol features 223
14.2 Motivating example: a client/server protocol 224
14.3 Properties of model program composition 241
14.4 Modeling techniques using composition and
features 245
14.5 Exercises 246
15 Modeling Objects 247
15.1 Instance variables as field maps 247
15.2 Creating instances 249
15.3 Object IDs and composition 253
15.4 Harnessing considerations for objects 254
15.5 Abstract values and isomorphic states 256
15.6 Exercises 257
16 Reactive Systems 259
16.1 Observable actions 259
16.2 Nondeterminism 261
16.3 Asynchronous stepping 264
16.4 Partial explorability 265
16.5 Adaptive on-the-fly testing 268
16.6 Partially ordered runs 272
16.7 Exercises 274
17 Further Reading 275
x Contents
V Appendices
A Modeling Library Reference 281
A.1 Attributes 282
A.2 Data types 292
A.3 Action terms 306
B Command Reference 308
B.
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