13 Further Reading
There are many existing formal methods that support modeling and analysis with
complex state, including Alloy (Jackson, 2006), ASMs (Gurevich, 1995; B??orger
and St??ark, 2003), B (Abrial, 1996), Promela (Holzmann, 2004), TLA (Lamport,
2002), Unity (Chandy and Misra, 1988), VDM (Fitzgerald and Larsen, 1998), and
Z (Woodcock and Loomes, 1989; Spivey, 1992; Davies andWoodcock, 1996; Jacky,
1997). Case studies in these methods demonstrate many ways to use sets, bags,
sequences, maps, and other data types similar to the ones in the modeling library.
AsmL (abstract state machine language) (Gurevich et al., 2005) includes highlevel
data structures like sets and maps and builds on the theory of partial updates
(Gurevich and Tillmann, 2005) that allows pointwise changes to such data structures
that may, moreover, be nested. AsmL was first supported in the model-based testing
tool AsmL-T (Barnett et al., 2003) and is also supported in the Spec Explorer
tool (SpecExplorer, 2006). Spec Explorer also supports an extension of the Spec#
language (Barnett et al., 2005) with high-level data structures such as sets and maps.
The pruning techniques discussed in Section 11.2 are mostly based on work that
was done in Spec Explorer (Veanes et al., in press). The use of composition in this
context is based on Veanes et al. (2007a). The state grouping technique discussed
in Section 11.
Pages:
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295