We all depend constantly on the reliability of computers and the devices that they control. And we fully expect that these systems will work properly when needed, despite that fact that computer programs often have hidden bugs that can disrupt their operation.
Why, then, are there not more frustrating or even life-threatening failures of the critical computerized mechanisms on which we rely?
Part of the answer is in the use of a computer hardware and software quality assurance verification technique known as model checking.
Three computer scientists – Edmund M. Clarke, E. Allen Emerson and Joseph Sifakis – developed this technique in the early 1980s by initially applying it to temporal logic formulae representing various sequences of events – and then with their colleagues extending its use to both complex and real-time systems.
Model checking has since become the most popular verification technique for correcting errors in the hardware and software designs of complex computer components and systems.
This month, the contributions of Clarke, Emerson and Sifakis were recognized when the Association for Computing Machinery announced that they would receive the 2008 A. M. Turing Award. Named in honor of mathematician Alan Turing, this award is considered the equivalent of the Nobel Prize for those in the computer field. It includes a cash prize of $250,000, with financial support provided by Intel Corp. and Google Inc.
In essence, model checking simply means that an abstract representation of a software or hardware design and its underlying logic is tested to ensure that its behavior will satisfy performance expectations. The model, reflecting the desired system requirements, must be formulated with sufficient clarity and properly structured so that the designers can evaluate its performance under varying operating conditions.
This technique uses algorithms or logical step-by-step procedures for solving problems, together with often novel data structures, to produce one of two possible outcomes when applied to a proposed model.
One result is that the performance of the model does indeed satisfy the designers’ expectations and therefore is a success. The other outcome takes the form of a counterexample, which corresponds to unexpected or undesirable system responses (for example, the computer-controlled automated safety device fails).
This counterexample is valuable because it then is used to determine the unknown source of the error embedded within the software or hardware of the design. When this core fault is identified, the designers can work to correct the model and ensure that the final system will behave properly during use.
Model checking is a method that has proven to be faster and less expensive than other techniques used to debug computer components and devices because it can be used during development.
Logical errors in software algorithms, integrated circuits and other system elements can be rectified early without severely delaying implementation plans or placing users in jeopardy.
Most important, the technique provides both the designers and the users of safety-critical devices with greater confidence that these computerized mechanisms will operate properly when needed.