Browse Books

Reviewer: Simon John Thompson

Verification is the process of showing that a system meets aspects of its specification by means of logical reasoning. As the author states, the field ranges from pencil-and-paper proof, through machine-assisted verification in which substantial amounts of bookkeeping and checking are automated, to fully automatic verification. General logical validity is undecidable, forcing some degree of human intervention, but many subproblems are decidable, which allows for machine implementation of the verification problem. In the introduction, the author provides a useful survey of techniques in this area, including model checking and binary decision diagrams. His approach is one of automata-theoretic verification, in which it is shown that the behaviors of an implementation all meet the constraints of the specifi cation, which is itself expressed as an automaton. The system uses omega-automata, whose infinite behaviors are capable of describing liveness as well as invariant properties, permitting the verification of substantial practical constraints. In order to make verification tractable as well as decidable, limited formalisms are often used. The author's approach is different, and accords with common sense. He seeks to reduce the verification problem to a collection of simpler tasks, by a two-stage process. First a property is decomposed into a collection of local properties, then the localization of the full problem to each of these local properties replaces the original test by a computationally more tractable one. Of course, it is in the selection of the decomposition that the difficulty lies; the author offers various heuristics, but also says that “the general problem of how best to decompose a task into more local subtasks is an important open problem.” Nevertheless, this work offers substantial insight into the verification process. The author presents introductions to the theory of omega-automata as well as B oolean algebra before embarking on the main topics, making the book a self-contained introduction for anyone familiar with the fundamentals of the theory of machines. The book is well indexed and contains a substantial bibliography, as well as pointing to the implementation of the verification techniques in the COSPAN system.