Model Checking: Algorithmic
Verification and Debugging
By Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis
1. e. aLLen emeRson
moDeL checKinG: a BiRD’s-e Ye Vie W
1. 1. formal Verification
Formal verification of program correctness hinges on the
use of mathematical logic. A program is a mathematical
object with well-defined, although possibly complex and
intuitively unfathomable, behavior. Mathematical logic
can be used to describe precisely what constitutes correct
behavior. This makes it possible to contemplate mathematically establishing that the program behavior conforms to the correctness specification. In most early work
this involved constructing a formal proof of correctness.
In contradistinction, model checking avoids proofs.
Floyd-Hoare-style deductive verification was the prevailing mode of formal verification going back to the 1960s.
This classic and elegant approach entailed manual proof
construction, typically using axioms and inference rules in
a formal deductive system, often oriented toward sequential programs. Such proof construction was tedious, difficult, and required human ingenuity. This field was a great
intellectual success, spawning work on compositional or
modular proof systems, soundness of program proof systems, and their completeness; see Section 3. Case studies
confirmed that this approach really worked for small programs, although a short program might require a long proof.
However, manual verification did not scale up well to large
programs. The proofs were just too hard to construct.
1. 2. temporal Logics
In view of the difficulties in trying to construct program
proofs it seemed like there ought to be a better way. The way
was inspired by the use of Temporal Logic (TL), a formalism
for describing change over time. If a program can be specified in TL, it can be realized as a finite state system. This suggested the idea of model checking—to check if a finite state
graph is a model of a TL specification.
The critical suggestion of using TL for reasoning about
ongoing concurrent programs was made in Pnueli’s landmark paper.
39 Such systems ideally exhibit nonterminat-ing behavior so that they do not conform to the Hoare-style
paradigm. They are also typically nondeterministic.
Examples include hardware circuits, microprocessors,
operating systems, banking networks, communication
protocols, automotive electronics, and many modern
medical devices. Pnueli used a TL with basic temporal
operators F (sometime) and g (always). Augmented with x
(next-time) and u (until), this is today known as LTL (Linear
Time Logic).
Another widely used logic is CTL (Computation Tree
Logic)
10 (cf. Emerson and Clarke, and Ben-Ari et al.
20, 4). Its
basic temporal modalities are a (for all futures) or e (for
some future) followed by one of F (sometime), g (always),
x (next-time), and u (until); compound formulae are built
up from nestings and propositional combinations of CTL
subformulae. CTL is a branching time logic as it can distinguish between aFp (along all futures, P eventually holds and