In the next example we take advantage of this to reveal the safety violations in the
reactive system that we exposed by a different technique in Chapter 6, Section 6.3.1.
Recall that we had to write a Boolean expression that described the safe states. Now
we will describe the safety violation in terms of actions, not states.
A safety violation occurs if the program performs a calibration after it receives a
message that contains an out-of-range temperature. In order to enable the calibration,
the program must first receive an in-range temperature. The safety violation can be
described by a scenario that contains just those three actions:
FSM(0,AcceptingStates(),Transitions(
t(0,Message("99.9"),1),
t(1,Message("999.9"),2),
t(2,Calibrate(),3)))
It is not necessary to include any other action in the scenario, because they will
be filled-in by interleaving when we compose the scenario with the contract model
program. Recall that any actions that are not explicitly included in the vocabulary of
the scenario model program can interleave among its actions when it is composed.
Here we make use of that fact to complete the runs. Many interleavings are possible,
so this scenario describes many runs.
We compose this scenario machine (whose FSM appears in Figure 7.18) with
the contract model program (whose FSM, with unsafe states highlighted, appears in
Figure 6.
Pages:
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199