In this chapter we show how model-based analysis reveals the design errors in
the reactive system we discussed in Chapter 3, by exploring the model program we
developed in Chapter 5, Section 5.7. We explain and demonstrate safety analysis
that identifies unsafe (forbidden) states and liveness analysis that identifies dead
states from which goals cannot be reached. Dead states indicate deadlocks (where
the program seems to stop running and stops responding to events) or livelocks
(where the program keeps running but can??™t make progress).
In this chapter we also introduce the mpv (Model Program Viewer) tool for
visualization and analysis, and explain how to use the modeling library features that
support analysis.
6.1 Finite state machines
In this section we motivate and explain FSMs.
Simulation is the most limited and labor-intensive model-based analysis technique
because it only considers one run at a time (Chapter 5, Section 5.5). To
perform more thorough analyses ??“ to detect the design errors discussed in Chapter
3, for example ??“ we need to consider many different runs. The obvious way
would be to code a large number of runs, but this is not a practical solution. In order
to get good coverage of program behaviors, wewould usually have code a great many
runs, and some would be very long. But the collection of runs would be redundant.
The same sequences of actions would appear again and again in different runs, and
even within a single run.
Pages:
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143