16. Newsreader scenario FSM for analysis by composition.
0
1
ShowTitles()
2
SortByFirst()
Figure 7.17. News reader scenario FSM, incomplete projection after composition.
might interleave anywhere among the actions of the scenario. Defining the scenario
vocabulary as we do here prevents these unwanted interleavings from confusing the
analysis.
Figure 7.16 shows the FSM for this scenario. We compose this with the contract
model program (whose FSM is shown in Chapter 6, Figure 6.2). Figure 7.17 shows
the projection of the product onto the scenario. The projection is incomplete; it only
includes the first two transitions of the scenario. This shows that the contract model
program cannot execute this scenario, because the third transition of the scenario is
not enabled in the contract model program. It was at this point that the simulation
failed (Chapter 5, Section 5.5). The FSM of the product shows the same thing, but
the product sometimes contains additional transitions that make it harder to interpret,
so we recommend inspecting the projection for this analysis.
134 Structuring Model Programs with Features and Composition
0
1
Message("99.9")
2
Message("999.9")
3
Calibrate()
Figure 7.18. Reactive system: scenario FSM for safety analysis.
The preceding example resembles simulation or interactive exploration in checking
just one run. But a scenario model program can describe more than one run.
Pages:
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198