We find that expressing the models in a familiar
programming language brings them within reach of most people involved in the
technical aspects of software production. We also find that focusing on testing as
xiv Preface
one of the main purposes of modeling provides motivation, direction, and a practical
emphasis that developers and testers appreciate.
This book is divided into four parts. The end of each part is an exit point; a
reader who stops there will have understanding and tools for modeling, analysis,
and testing up to that level of complexity. Presentation is sequential through Part III,
each chapter and part is a prerequisite for all the following chapters and parts.
Chapters in Part IV are independent; readers can read one, some, or all in any order.
This book provides numerous practical examples, case studies, and exercises and
contains an extensive bibliography, including citations to relevant research papers
and reports.
Acknowledgments
Parts of this book were written at Microsoft Research. The NModel framework was
designed and implemented at Microsoft Research by Colin Campbell and Margus
Veanes with graph viewing functionality by Lev Nachmanson.
The ideas in this book were developed and made practical at Microsoft Research
from 1999 through 2007 in the Foundations of Software Engineering group.
Contributors included Mike Barnett, Nikolaj Bjorner, Colin Campbell, Wolfgang
Grieskamp, Yuri Gurevich, Lev Nachmanson, Wolfram Schulte, Nikolai Tillman,
Margus Veanes, as well as many interns, in particular Juhan Ernits, visitors, university
collaborators, and colleagues from the Microsoft product groups.
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