In particular, creation of a new
object corresponds to importing of a reserve element. The support for modeling with
objects was already supported in the AsmL-T tool (Barnett et al., 2003) that is the
predecessor of Spec Explorer. Support for dynamic object graphs was also present
in the Agedis tools (Hartman and Nagin, 2004).
The state isomorphism problem discussed in Section 15.5 arises when unordered
data structures and objects are combined and is as hard as graph isomorphism
(Ullmann, 1976; McKay, 1981). The problem occurs very frequently. Already the
standard Spec Explorer example known as the chat system uses objects as well as
sets and maps; see Utting and Legeard (2006, Section 6.5) for a detailed exposition
of this example. The state isomorphism problem was not solved in Spec Explorer.
If objects are not used, then state isomorphism reduces to state equality that can
be checked in linear time. This is possible because the internal representation of
all data structures can then be canonicalized. The same argument is true if objects
are used but all data structures are ordered. Then state isomorphism reduces to
heap canonicalization in the context of model checking and can be implemented in
linear time (Iosif, 2004; Musuvathi and Dill, 2005). Bogor (Robby et al., 2006) is a
customizable software model checking engine that uses the method of Iosif (2004)
to perform heap canonicalization based on an ordering of object ids.
Pages:
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366