Korat (Boyapati
et al., 2002) is a tool for automated test generation based on Java specifications. It also
uses the concept of heap isomorphism. Symstra (Xie et al., 2005) uses a technique
Advanced Topics 277
that linearizes heaps into integer sequences to reduce checking heap isomorphism
to just comparing the integer sequence equality. A survey of symmetry reductions
in temporal logic model checking is given in Miller et al. (2006). The general state
isomorphism problem and more related work is discussed in Veanes et al. (2007b).
Reactive systems. The idea of on-the-fly testing was pioneered in the context of
labeled transition systems using the IOCO theory (Tretmans and Belinfante, 1999;
Brinksma and Tretmans, 2001; van der Bijl et al., 2004) and has been implemented in
tools such as TorX (Tretmans and Brinksma, 2003) and TGV (Jard and J??eron, 2005).
IOCO theory is a formal testing theory based on LTSs with input actions and output
actions, where input actions correspond to controllable actions and output actions
correspond to observable action as discussed in Section 16.1. The IOCO theory
is closely related to refinement of interface automata (de Alfaro and Henzinger,
2001; de Alfaro, 2004) that is based on the notion of alternating refinement (Alur
et al., 1998). Refinement of interface automata supports the view of testing as a
game between a tester and the IUT and is used as the basis for the conformance
relation implemented in the Spec Explorer tool (Veanes et al.
Pages:
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367