And, the liveness requirement is: the calibrate action
should follow the arrival of a command. A property expressed in this way, by
describing the ordering of actions, is a temporal property.
Scenario model programs can express temporal properties, and composition can
check them. Compose the contract model program with the scenario model program
that expresses the property. Examine the projection of the product onto the scenario.
If the projection is complete (it contains all of the transitions of the original scenario
model program), then the contract model program can execute that scenario, and
you will be able to find the runs of the scenario in the product. If the projection is
incomplete (if it is missing some transitions), then the contract model program cannot
execute that scenario, and you will not find any runs of the scenario in the product.
Notice how this use of composition differs from scenario control, where we write
a scenario that we want the contract model program to execute, that we assume it
can execute. For analysis, we write a scenario that the contract model program may
not be able to execute; that is what we want to find out.
Let??™s look at some examples. First, we consider an example where the scenario
model program describes exactly one run. The analysis tells us whether the contract
model program can execute that run; it provides the same information as simulation
(Chapter 5, Section 5.
Pages:
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196