Execute this test suite on the implementation from Chapter 3 (with
unsafe states and dead states) and on the revised implementation you wrote for
Exercise 3 (without unsafe states and dead states) in Chapter 3.
5. Could you use ct as a unit testing tool, as an alternative to NUnit? How? What
would correspond to a test and a test fixture?
9 Further Reading
There are many modeling languages based on guarded update rules (or something
similar), 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 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.
Pages:
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219