246 Compositional Modeling
For parameter generation one can also use dependent features of model programs
if parameter selection is most conveniently done by reading the state of the contract
model program.
14.4.4 Property checking
One can write a model program to describe a temporal property that describes a ???bad???
behavior of the contract. For example, a certain pattern of actions leads to a state
where a safety condition in the property model program is violated. Composition of
the contract model program with the property model program can be explored for
safety analysis (as we demonstrated in Chapter 7, Section 7.5).
One can also write a state-dependent condition in a separate feature that reads
state variables of multiple features and defines a global safety condition spanning
those features. It is asssumed here that the feature model programs use distinct state
variables, so the safety condition is not specific to any single feature model program.
14.4.5 State refinement
One can use composition to abstract details of subbehaviors. The idea is the following.
Suppose you have a model program A that includes two actions StartB() and
FinishB(). There is another model program B that describes the behavior of B. The
only action symbols that A and B have in common are StartB() and FinishB(). When
A is explored in isolation, then StartB() leads to a state "B-Is-Working" where the
only enabled action is FinishB().
Pages:
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327