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).
The classic books on testing are by Myers (1979) Myers et al. (2004), and
Beizer (1984, 1990, 1995). Poston (1996) surveys and collects some early papers on
what we now call model-based testing. Binder (1999) adds special consideration for
object-oriented programs. Kaner et al. (1993) emphasize the pragmatics of testing
desktop applications, including business considerations. Peled (2001) also discusses
150
Systems with Finite Models 151
testing. All of these books have voluminous bibliographies up to their publication
dates.
The review article by Lee and Yannakakis (1996) discusses generating tests from
FSMs, including the postman tour. Peled (2001) also discusses the postman tour.
Thimbleby (2003) presents a complete implementation of the postman tour.
Pages:
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220