[Postscript version of this page]
With the increasing complexity of systems designed today, the problem of design verification is becoming harder. It is my belief that formal methods can be used to make this task easier.
Model checking has been extremely useful in proving correctness properties and finding violations of those for finite state systems. The key ingredient that makes model checking successful is that it is automatic. The tool takes a system and a property to check and automatically either proves it correct or comes up with a violation.
However model checking is not directly applicable to infinite, or unbounded, state systems and also to large finite state systems. Systems with unbounded state could arise if we have parameterized systems where the parameter could take on any value. Also, the design might be described with unbounded data types, like bignums and message queues. For such systems, theorem proving has been relied on.
Traditional theorem proving methods, though extremely powerful, need human guidance. Much of it is conceptually simple, but tedious and repetitive, for the user. Combining the power of theorem proving methods with the automation of model checking will make formal methods much more useful.
I would like to work on combining different formal method techniques to handle large designs either automatically, or with less manual intervention. My research as part of PhD thesis has been to combine model checking with theorem proving by the use of Predicate Abstraction.
Predicate abstraction is a technique that is usually used to prove properties of infinite state systems. It is a combination of theorem proving and model checking techniques. Given a concrete infinite state system and a set of abstraction predicates, a conservative finite state abstraction is generated. It is conservative in the sense that for every execution in the concrete system there is a corresponding execution in the abstract system. The abstract version of the verification condition is model checked in this abstract system. If the property is verified then it holds in the concrete system. Otherwise an abstract counter-example trace is generated. There could be a concrete counter-example corresponding to it, in which case there is a bug in the design, or the abstract counter-example is an artifact of the abstraction. Our tool can automatically analyze the counter-example to find a real bug or to suggest extra predicates to refine the abstraction thereby avoiding that particular spurious trace. Then the process starts anew. This process is not guaranteed to terminate, after all proving arbitrary safety properties of an infinite state system is not decidable, but for a large number of problems this method can successfully prove properties.
The prototype verification tool is written in Common Lisp. It uses Binary Decision Diagrams to implement the model checker and to represent the abstract system. Satisfibility checks of logic formulas over the concrete domain are carried out with CVC.
In addition to a lot of standard mutual exclusion algorithms, this method has been applied with varying degrees of automation to the following problems:
The PredicateAbstractionExamples page has a listing of protocols that we have applied our tool to.
As part of a summer job at Microsoft Research, I worked on the SLAM Project The aim of the SLAM project is to prove correctness properties of OS device drivers by using predicate abstraction. As described above, predicate abstraction consists of two steps -- creating an abstract system and then model checking it. Creating the best possible abstract system is expensive. Often an approximation, which can be generated more easily, is sufficient to prove the desired property. So instead of creating the most accurate model possible at the outset, an approximation of the abstract system is generated which is then refined as needed. This allows SLAM scale to larger problems enabling its use to tackle larger device drivers.