I am not competent to discuss model checking at any level, and so I asked someone who is ! Ganesh Gopalakrishnan is a colleague of mine at the U. and heads our Formal Verification group. I asked him if he could write a perspective on model checking, and he kindly agreed. What follows is his piece (with URLs added by me). As usual, all credit to him, and any mistakes in transcribing are my fault alone.
A Perspective On Model Checking
Ganesh Gopalakrishnan
One of the earliest attempts at proving the correctness of a program was by Alan Turing in 1949. The activity was raised to a much more prominent level of interest and importance through the works of Dijkstra, Hoare, and others. Yet, the enterprise of "Program Verification" was met with more noticeable failures than successes in the 1970's, due to its inability to make a dent on practice. The introduction of Temporal Logic for modeling concurrent systems (for which Amir Pnueli won the 1996 Turing Award) was the first attempt at shifting the attention away from the impossibly difficult task of 'whole program verification' to a much more tractable focus on verifying the reactive aspects of concurrency.
Looking back, this enterprise did not meet with the expected degree of success, as Temporal Logic reasoning was still based on `deduction' (proof from first principles). From an engineer's perspective, what was needed was a simple way to specify the classes of "legal and illegal waveforms" a system can produce on its signals / variables, and an efficient way of checking that all those waveforms are contained in the set of "legal waveforms" as can be specified through temporal properties. In other words, it was sufficient to show that finite state machines (or finite state control skeletons of programs) served as *models* for a catalog of desired temporal properties.
This was essentially the approach of model checking. It immediately took off as a practically viable method for debugging concurrent systems; the approach guaranteed exhaustive verification for small instances of a problem. In practice it meant that all relevant corner cases were considered in the confines of afforable resource budgets. This was the gist of Allen Emerson's contribution in his PhD dissertation which he wrote under Ed Clarke's guidance. A parallel effort underway at France in Joseph Sifakis's group also arrived at the same pragmatic approach to verification. Model checking was given crucial impetus by Ken McMillan who, using the technology of Binary Decision Diagrams formulated and popularized by Randy Bryant, developed the highly efficient Symbolic Model Checking approach. The technology has since then skyrocketed in its adoption rate.
Today, model checking and its derivatives are part of every verification tool used to debug digital hardware. While "full verification" is not the goal (and is largely a meaningless term), the ability of model checkers to find *high quality bugs* is uncanny. It is those bugs that escape simulation, and may not even manifest in hardware that operates at the rate of GHz. Some of the error traces produced by model checkers are only about two dozen steps long; yet, if one imagines the number of reachable nodes in a tree with arity (branching factor) 2000 in two dozen steps, one understands why conventional approaches to testing miss bugs: they have to make the same lucky "1 in 2000" choices two dozen times in a row. A model checker can often get away by not really modeling these choices explicitly. Reduction techniques allow model checkers to detect and avoid exploring many "equivalent" behaviors. In that sense, model checking is one of the most powerful "test acceleration technologies" that mankind has invented.
Today, microprocessor companies employ several kinds of model checkers. In software, Bell Labs (mainly before its collapse), JPL, NASA, and Microsoft (to name a few) have had tremendous success using model checking for verifying device drivers, switch software, and flight control software. Speaking more generally, anything with a finite state structure (e.g., decision processes, reliability models, planning in AI) can be approached through model checking.
Aftermatter:
- Daniel Jackson (MIT), "With its dramatic successes in automatically detecting design errors (mainly in hardware and protocols), model checking has recently rescued the reputation of formal methods." (source)
- "Proofs of programs are too boring for the social process of mathematics to work." DeMillo et al in CACM 1979).
No comments:
Post a Comment