Moreover, our methods can sometimes achieve better coverage in
less testing time than do hand-coded tests.
Testing (i.e., executing code) is not the only assurance method. Some software
failures are caused by deep errors that originate in specifications or designs. Model
programs can represent specifications and designs, and our methods can expose
problems in them. They can help you visualize aspects of system behavior. They
can perform a safety analysis that checks whether the system can reach forbidden
states, and a liveness analysis that identifies dead states from which goals cannot
be reached, including deadlocks (where the program seems to stop) and livelocks
(where the program cycles endlessly without making progress). Analysis uses the
same model programs and much of the same technology as testing.
This book is intended for professional software developers, including testers,
and for university students in computer science. It can serve as a textbook or
supplementary reading in undergraduate courses on software engineering, testing,
xi
xii Preface
specification, or applications of formal methods. The style is accessible and the
emphasis is practical, yet there is enough information here to make this book a
useful introduction to the underlying theory. The methods and technology were
developed at Microsoft Research and are used by Microsoft product groups, but this
book emphasizes principles that are independent of the particular technology and
vendor.
Pages:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25