Formal Verification

Therac-25 was a medical particle accelerator. A race condition in its software killed three patients. The bug lived in the code for years and the tests never caught it. Formal verification would have found it in minutes.

• Amazon AWS verified 16 distributed systems in TLA+ and found 10 critical bugs in the specifications before implementation
• Intel adopted model checking for the FPU after the Pentium FDIV bug cost the company $475M. The Pentium 4 was formally verified
• NASA Deep Space 1 and Mars Pathfinder were verified with SPIN before launch
• Microsoft verified USB drivers and the NTFS file system using SLAM/SDV (Software Device Verifier)
• Airbus A380 fly-by-wire software was verified with Simulink Design Verifier and Polyspace

Model Checking

Model checking is the automatic verification of finite systems: the algorithm walks the state graph and checks whether the specification holds on every reachable path.

The core problem is state-space explosion: a system with 100 boolean variables has 2^100 states. BDDs (Binary Decision Diagrams) and symbolic model checking let you work with exponential state spaces compactly.

• Safety: 'something bad never happens' - invariants
• Liveness: 'something good eventually happens' - progress
• Fairness: 'a process gets the resource infinitely often' - scheduler
• SPIN: a Promela model verifier, used on the NASA Mars Pathfinder
• CBMC: a bounded model checker for C/C++, finds buffer overflows

TLA+ and Specifications

TLA+ (Temporal Logic of Actions) is Leslie Lamport's specification language. Amazon uses TLA+ to verify distributed protocols: DynamoDB, S3, and EBS were checked with it and real bugs were found.

TLA+ models a system as a sequence of states. Formulas describe the allowed transitions (Next) and invariants. The TLC model checker explores every reachable state of the model.

• TLA+ applied at Amazon (16 systems, 10 bugs found in specifications)
• Microsoft uses P (a language similar to TLA+) for verifying the USB stack
• Intel used model checking to verify the Pentium FPU after the FDIV bug
• Azure Cosmos DB is verified in TLA+

SPIN and Promela

SPIN (Simple Promela INterpreter) is Gerard Holzmann's protocol verifier, developed at Bell Labs. It was used to verify NASA's Deep Space 1, the Mars Pathfinder, and 802.11 protocols.

SPIN uses on-the-fly model checking: the LTL formula is converted into a Büchi automaton, whose synchronous product with the model is checked for language emptiness. This avoids constructing the full state space explicitly.

• Promela (Protocol Meta Language) is a language for describing concurrent processes
• LTL to Büchi: the formula [] p produces an automaton accepting all infinite words where p always holds
• Partial order reduction: shrinks the state space by ignoring independent steps
• Bit-state hash compression: stores visited states in a Bloom filter (false negatives are possible)

Temporal Logic: LTL and CTL

Temporal logic extends classical logic with time operators. There are two main flavors: LTL (Linear Temporal Logic) reasons about paths; CTL (Computation Tree Logic) reasons about computation trees.

• LTL and CTL are incomparable: some properties are expressible in one but not the other
• AG EF reset (CTL) cannot be expressed in LTL: it quantifies over paths from any state
• G (F p) (LTL) cannot be expressed in CTL: a path where p holds infinitely often
• CTL* subsumes both: PSPACE-complete like LTL
• The mu-calculus is the most expressive temporal logic and includes CTL and LTL

Key Takeaways

• Model checking is automatic state-graph exploration, bounded by state-space explosion
• TLA+ models systems as sequences of states with temporal properties
• SPIN compiles Promela + LTL into a C verifier with an on-the-fly algorithm
• LTL reasons about linear paths, CTL about computation trees; the two are incomparable

Related Topics

Formal verification sits at the intersection of automata theory, complexity theory, and mathematical logic:

• Büchi automata — SPIN translates LTL into Büchi automata to verify infinite paths
• PSPACE-complete — LTL model checking is PSPACE-complete, CTL is in P. Hence different tools
• Lattice theory — The mu-calculus is built on Tarski's fixed-point theorem on lattices
• Typed lambda calculus — Coq and Lean realize Curry-Howard: types are theorems, programs are proofs

Вопросы для размышления

• Why has formal verification not replaced testing in most projects?
• Is it better to verify the specification or the implementation? What are the limits of each approach?
• How does partial order reduction help with state-space explosion in concurrent systems?

Связанные уроки

• ml-04
• ml-02