When this happens, the number of transitions
found equals MaxTransitions. You may also notice unexpected dead ends in
the graph. In that case, you should increase MaxTransitions and explore again.
Many analysis questions can be expressed in terms of safety or liveness. In the
following subsections we use safety and liveness analyses to reveal design errors in
the reactive system we discussed in Chapter 3, whose model program we developed
in Chapter 5, Section 5.7.
6.3.1 Safety
Safety analysis checks whether anything bad can happen. It searches for unsafe
states that violate safety requirements. We express safety requirements by writing
a Boolean expression called an invariant, which is supposed to be true in every
state that can be reached. An unsafe state is a state where an invariant is false.
For the tools, an invariant is a Boolean field, property, or method labeled with the
[StateInvariant] attribute.
Safety analysis depends on writing an invariant that expresses the safety property
we wish to check.We must consider which states are allowed (that make the invariant
true) and which are forbidden (that make the invariant false). Identifying the safe
states requires judgment and understanding the program??™s purpose.
Recall that the purpose of our reactive system is to perform a calibration with
a valid temperature sample. Performing a calibration with an invalid temperature
sample would be bad.
Pages:
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162