14.3.3 Trace inclusion
For scenario control, it is sometimes useful to refer to the state variables of a feature
of a model program in order to write a scenario for it. In other words, there is a given
model program M with a feature F1 that is the contract and there is a dependent
feature F2 of M that may read the state variables of F1 but it may not change the
values of those variables. A property that is preserved in this case is that the set of
traces of M[F1] is a superset of the set of traces of M[F1, F2]. Such use of features
is usually safe because no new traces can arise.
Two typical uses of dependent features for scenario control are state-dependent
parameter generation and enabling condition strengthening. Both uses were illustrated
earlier in this chapter with the CreditScenario scenario in Figure 14.16.
Advanced Topics 245
14.4 Modeling techniques using composition and features
Composition and features can be used for many different purposes. This has been
illustrated with numerous examples in the book. In this section we provide a brief
summary of the techniques according to the following topics:
??? Feature-oriented modeling
??? Scenario control
??? Parameter generation
??? Property checking
??? State refinement
14.4.1 Feature-oriented modeling
This was the main topic of this chapter. The idea is that a large system is divided
into separate features.
Pages:
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325