Here in Part II, we explain modeling, analysis, and testing with finite model
programs that can be analyzed exhaustively (completely). The programs and systems
we model here are ???infinite??? ??“ perhaps not mathematically infinite, but too large to
analyze exhaustively. One of the themes of this chapter is how to finitize (make
finite) the model of an ???infinite??? system. Starting in Part III, the model programs are
also ???infinite???; we finitize the analysis instead.
In this chapter we develop and explain three model programs: a newsreader
user interface, the client/server system of Chapter 2, and the reactive system of
Chapter 3. We will perform safety and liveness analyses of the reactive system
model in Chapter 6. We will generate and check tests of the implementation using
the client/server model in Chapter 8.
5.1 States, actions, and behavior
First we must define some basic concepts and vocabulary.We will demonstrate these
concepts in the sections that follow.
A model program is a program that describes the behavior of another program or
system called the implementation. We say system here because the implementation
need not be a single program. A single model program can represent a concurrent
57
58 Model Programs
system comprising several programs, or a distributed system that includes several
computers connected by a network. A model program can also represent the environment
where the implementation runs, including messages in transit between
networked computers, or events originating in attached hardware.
Pages:
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97