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