complexity of satisfiability for these logics was the major
focus. However, model checking refers to the truth under
one given interpretation M of a given formula f. This notion
was implicit in the Tarskian definition of truth but, classically, was not viewed as an interesting problem. The idea
that model checking should provide for verification of finite
state systems was not appreciated. The early reaction to
model checking then was mostly one of confusion and disinterest. It seemed a disconcerting novelty. It was not satisfiability. It was not validity. What was it? It was even dubbed
“disorienting.” Many felt it could not possibly work well in
practice. In more recent times, some more favorable comments have been made. Model checking is “an acceptable
crutch”—Edsger W. Dijkstra; it is “a first step toward engi-neerization of the field”—A. Pnueli.
40
What factors contributed to model checking’s successful deployment? First, the initial framework was feasible
and comprehensible. It built on a helpful combination of
TL and algorithms. It provided a “push-button,” i.e., automated, method for verification. It permitted bug detection as well as verification of correctness. Since most
programs are wrong, this is enormously important in
practice. Incidently, the limited support for bug detection
in proof-theoretic verification approaches contributes to
their slower adoption rate. Moreover, while a methodology of constructing a program hand-in-hand with its proof
certainly has its merits, it is not readily automatable. This
hampers its deployment. With model checking, the separation of system development from verification and debugging (see Section 2) has undoubtedly facilitated model
checking’s industrial acceptance. The development team
can go ahead and produce various aspects of the system
under design. The team of verifiers or verification engineers
can conduct verification independently. Hopefully, many
subtle bugs will be detected and fixed. As a practical matter, the system can go into production at whatever level of
“acceptable correctness” prevails at deadline time. Lastly,
Moore’s Law has engendered larger computer main memory, which enabled the development of ever more powerful
model checking tools.
1. 7. Discussion and summary
What are the key accomplishments of model checking?
The key contribution is that verification using model
checking is now done routinely on a widespread basis
for many large systems, including industrial-strength
systems. Large organizations from hardware vendors to
government agencies depend on model checking to facilitate achieving their goals. In contrast to 28 years ago, we
no longer just talk about verification; we do it. The somewhat surprising conceptual finding is that verification can
be done extremely well by automated search rather than
manual proofs.
Model checking realizes in small part the Dream of
Leibniz [1646–1716] (cf. Davis18). This was a proposal for
a universal reasoning system. It was comprised of a lingua
characteristica universalis, a language in which all knowledge could be formally expressed. TL plays a limited
formulation of this role. There was also a calculus ratiocinator, a method of calculating the truth value of such
a formalized assertion. Model checking algorithms provide
the means of calculating truth. We hope that, over time,
model checking will realize an increasingly large portion
of Leibniz’ Dream.
2. eDmunD m. cLaRKe
m Y 28-YeaR Quest to conQueR
the state exPLosion PRoBLem
2. 1. model checkers and Debugging
Model checkers typically have three main components:
( 1) a specification language, based on propositional TL,
39
( 2) a way of encoding a state machine representing the
system to be verified, and ( 3) a verification procedure, that
uses an intelligent exhaustive search of the state space to
determine if the specification is true or not. If the specification is not satisfied, then most model checkers will
produce a counterexample execution trace that shows
why the specification does not hold. It is impossible to
overestimate the importance of this feature. The counterexamples are invaluable in debugging complex systems.
Some people use model checking just for this feature.
The EMC model checker11 did not give counterexamples
for universal CTL properties that were false or witnesses
for existential properties that were true. Michael C.
Browne added this feature to the MCB model checker in
1984. It has been an important feature of model checkers
ever since. (See Figure 2.)
figure 2. a model checker with counterexamples.
Preprocessor
Model checker
Formula f
Program or circuit