9 - Further Reading

Summary

There are many modeling languages based on guarded update rules (or something similar), including Alloy (Jackson, 2006), ASMs (Gurevich, 1995; Börger and Stärk, 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 and Woodcock, 1996; Jacky, 1997). Case studies in these languages show how different kinds of systems can be described in modeling styles similar to ours.

The immediate predecessors of the modeling library and tools described in this book are the AsmL language and the AsmL-T tool (Barnett et al., 2003), and more recently, the SpeC# language and the Spec Explorer tool (Veanes et al., in press; Campbell et al., 2005a). Development on Spec Explorer continues.

Peled (2001) presents an exhaustive exploration algorithm similar to ours. Grieskamp et al. (2002) describe a more complex exploration algorithm.

Exploration has some similarities to model checking, which also generates and explores a finite state machine (FSM), but usually emphasizes verifying (or providing counterexamples to) properties expressed as formulas in temporal logic. This is similar to our checking of temporal properties, but we express them with FSMs instead of formulas. Model checking was originally described by Clarke et al. (1986) in a classic paper and later described in a survey article (Clarke et al., 1994) and a book (Clarke et al., 1999). Some other model checkers are described in the books by Peled (2001) and Holzmann (2004).

Composition of model programs is a generalization of the construction of finite automata for the intersection of regular languages. For example, see the discussion following Theorem 3.3 on pp. 59–60 of Hopcroft and Ullman (1979).