It gives a
mathematical view of program state (including the state of object-oriented systems
and systems with complex structure). There is a well-developed body of scientific
literature on the topic. Readers interested in ASMs may wish to see the ASM Web
page maintained at the University of Michigan (ASM, 2006). Of particular interest
is the ???Lipari guide??? (Gurevich, 1995).
We also use ideas taken from finite automata, mathematical logic, and set theory.
The composition of automata for language intersection is a core concept.
A classic text that describes finite automata and their properties is Hopcroft and
Ullman (1979). A useful and practical introduction to logic and set theory is found
in Lipschutz (1998).
A mathematically rigorous survey of assurance methods including modeling,
testing, and static analysis appears in the book by Peled (2001).
The ideas in this book were developed and made practical at Microsoft Research
from 1999 through 2006 in the Foundations of Software Engineering group (FSE,
2006).
Other views of model-based testing appear in the books by Utting and Legeard
(2006) and by Broy et al. (2005). This is an active research area where new methods
and tools appear frequently. For a sample, see the papers by Tretmans (1999) and
Hartman and Nagin (2004), and the references cited therein.
Other work on particular aspects of modeling, testing, and analysis is discussed
and cited in the later Further reading chapters (Chapters 9, 13, and 17).
Pages:
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95