2.5 is introduced in Grieskamp et al. (2002). The algorithm is also
explained in B??orger and St??ark (2003, Section 3.2). The technique can be extended
to multiple groupings (Campbell and Veanes, 2005) that can be used to define
groupings per feature in a model program with multiple features. State grouping is
related to abstraction in model checking (Clarke et al., 1999).
Strategies for fully controlled systems is a special case of strategies for reactive
systems. In Yannakakis (2004) such strategies are classified as preset strategies
as opposed to adaptive strategies where (possibly nondeterministic) outputs of the
IUT may affect the strategy. (See also Chapter 17 in this connection.) The custom
strategy defined in Section 12.4.2 originates from Veanes et al. (2006).
The various notions of coverage mentioned in Section 12.4 are related to
correspodning classical notions of coverage in the context of black-box testing
219
220 Further Reading
(Beizer, 1995). Besides the use of composition, techniques discussed in Section 12.5
originate from Spec Explorer (Veanes et al., in press). The test execution algorithm
described in Section 12.5.2 is a special case of the algorithm described in Chapter 16.
(See also Chapter 17 in this connection.)
The book by Utting and Legeard (2006) describes several other model-based
testing tools, both commercial and noncommercial.
Pages:
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296