Here the bad thing is an action (performing a calibration) but
Systems with Finite Models 107
[StateInvariant]
public static bool CalibrateInRange()
{
return (!CalibrateEnabled()
|| buffer == InRange);
}
Figure 6.8. Reactive system: state invariant for safety analysis.
safety analysis requires that we identify states. We resolve this by describing the
states where the action is enabled, instead of the action itself. In the unsafe states, the
calibration action is enabled but the temperature is invalid. This Boolean expression
is true in the unsafe states:
CalibrateEnabled() && buffer != InRange // unsafe states
It is often easier to describe the unsafe states first, as we did here. Negate the
expression for unsafe states to obtain the safety condition.4
!CalibrateEnabled() || buffer == InRange // safety condition
We wrap this expression in a static method, label it with the [StateInvariant]
attribute, and place it in the Controller class in the Reactive model program
namespace (Figure 6.8).
Now that we have defined the state invariant, exploration can find all of the unsafe
states in the generated FSM.We command the mpv tool to explore the reactive system
model program, and to count and display unsafe states:
mpv /r:Controller.dll Reactive.Factory.Create /safetyCheckIsOn+ ...
Figure 6.9 shows the generated FSM.We had to increase MaxTransitions to 300
to generate the true FSM.
Pages:
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163