This book presents current methods for dealing with software reliability, illustrating the advantages and disadvantages of each method. The description of the techniques is intended for a non-expert audience with some minimal technical background. It also describes some advanced techniques, aimed at researchers and practitioners in software engineering. This reference will serve as an introduction to formal methods and techniques and will be a source for learning about various ways to enhance software reliability. Various projects and exercises give readers hands-on experience with the various formal methods and tools.
In addition to describing the individual methods in considerable depth, it
also discusses when each method is appropriate and the tradeoffs that are
necessary in selecting among them. The different techniques are illustrated
by many challenging exercises that can be used in conjunction with state of
the art tools. It even tells where to access the tools on the web! I do not know
of any other book that covers the same topics with such depth.
The book also describes the process of applying formal methods, starting
with modeling and specification, then selecting an appropriate verification
technique, and, finally, testing the resulting program. This knowledge is
essential in practice, but is rarely covered in software engineering texts. Most
books focus on a particular technique like program testing and do not cover
other validation techniques or how several techniques can be used in
combination. Because Doron has made significant contributions to the development
of many of the validation techniques described in the book, his insights are
particularly important on this critical issue.
The book is appropriate for a wide spectrum of people involved in the
development of software. It is particularly appropriate for an upper level
undergraduate level course on software reliability or a master's degree course
in software engineering. In fact, it is sufficiently well annotated with pointers
to other more advanced papers that it can be used as a reference source
for software engineers engaged in code validation or by researchers in formal
Having just completed a book on model checking with Doron, I am
immensely impressed with both his talent as a computer scientist and his skill
as a writer. I am sure that the present book will be an enormous success.
I recommend it with great enthusiasm for anyone who is interested in the
problem of software reliability.