Research in automatic program verification has been going on for decades, with few practical results. One line of investigation, however, has recently begun to yield fruit. If finite automata can model a system, and if the system’s important properties can be stated in temporal propositional logic expressions describing that automata, then tools can verify whether these properties hold for the automata. Such tools typically exhibit an execution sequence that shows how the description is violated if it does not hold, a great help in finding and fixing problems. Such verification tools are in fairly common use in some industrial settings, notably telecommunications and hardware design, and have found design errors that were otherwise undetected.

Using such automatic verification tools requires enormous expertise. Users must understand finite automata and be skilled in using them to model systems. They must also understand temporal propositional logic and be skilled in using it to state system properties. They must further understand the arcane verification tools currently available. And because it often happens that the automata are too large for the verification tools to handle, or program properties of interest cannot be expressed in the version of temporal logic processed by the verification tool, considerable ingenuity and skill must often be applied to rework the automata and the descriptions to make them tractable for the tool. Hence, there is need for texts like this one to help system developers gain the expertise required to take advantage of this technique.

This book has three parts. Part 1 contains introductory chapters on automata, temporal logic, basic model checking, symbolic model checking (a response to the state explosion problem encountered in basic model checking), and timed automata (an elaboration of finite automata for representing real-time systems).

Part 2 surveys mechanisms for describing system properties with temporal propositional logic. This section is organized into chapters based on a division of properties into reachability, safety, liveness, deadlock-freeness, and fairness. It concludes with a chapter on techniques for simplifying automata, while preserving their ability to model relevant properties of target systems.

Part 3 surveys six verification tools, one per chapter. The tools are all freely available over the Internet, and are fairly widely used. Each chapter describes a tool’s capabilities and limitations, automata and logic specification languages, verification capabilities, documentation quality, and case study availability, and lists references for the tool.

The book also includes a brief forward by Thomas Henzinger, a preface, a bibliography, and a short index.

The authors state that they intend this book to be an undergraduate text, a reference for professional engineers, and a source for researchers or graduate students familiarizing themselves with the field. The book would not make a good undergraduate text. It presumes great facility with automata and first-order logic, and an appreciation of complexity theory. The presentation is quite abstract, and requires considerable mathematical maturity. It has no exercises. For similar reasons, all but the most well-prepared professional engineers would probably find this book indigestible. Both of these audiences would be better served by other recent books, such as Peled, Grumberg, and Clarke [1] or Ryan and Huth [2].

On the other hand, researchers and graduate students, who presumably have stronger backgrounds in formal methods, should find this book useful as an overview of the field. It is short (190 pages), and well organized and cross-referenced. It has good examples and an informal conversational style. However, for a deeper understanding, other sources will have to be consulted. The authors could improve the book considerably by annotating the references, or by providing a short bibliographic essay on relevant literature.