Model checking with NuSMV: CTL and LTL logics, fixpoint algorithm and verification of mutual exclusion

A concurrent program, a communication protocol, the controller of a lift or of a traffic light can work for months and then get stuck in a combination of events that no test had tried. Formal methods verify a system exhaustively, proving that a property holds in all possible executions. There are two main roads: automated theorem proving, in which system and property are formulas of a logic and a proof is built, powerful but often in need of help from the user; and model checking, in which the system is a finite state machine, the properties are temporal logic formulas, and an algorithm explores all reachable states. This lesson explains model checking and the CTL and LTL logics, derives the fixpoint algorithm, and uses it with NuSMV, the symbolic model checker developed by FBK and the universities of Trento, Genoa and Carnegie Mellon, on a classic: mutual exclusion between two processes.

The idea in simple words

Imagine having to check that a crossroads with two traffic lights never shows green to both roads. Trying a few sequences of events by hand is not enough: the error could hide in a rare combination. Model checking builds the map of all the situations the system can be in (the states) and of all possible moves between them, and walks through it entirely looking for a forbidden situation. If it finds one, it returns the counterexample: the exact sequence of steps leading to the error, invaluable for fixing the design. If it does not, the property is proved for all executions.

The model: Kripke structures

The system is described as a Kripke structure: a finite set of states , initial states , a transition relation (from each state one can go to one or more next states) and, for each state, the set of atomic propositions true in it (for example “process 1 is in its critical section”). The executions are the infinite paths starting from an initial state; drawing them all from one state gives the computation tree.

The temporal logics CTL and LTL

Temporal operators talk about what happens along a path:

• : holds in the next state;
• : holds eventually (in the future);
• : holds always (globally);
• : holds until becomes true, and eventually becomes true.

LTL (linear temporal logic) evaluates these formulas on each path: an LTL formula holds if it holds on all paths. CTL (computation tree logic) puts a path quantifier in front of every operator: (for all paths) or (there exists a path). So says “in every reachable state holds” (a safety property: nothing bad ever happens), “there is a way to reach “, “on every path eventually holds” (a liveness property: something good eventually happens), “every request is eventually served”.

The algorithm: fixpoints

CTL model checking computes, for each subformula, the set of states where it holds, starting from the atomic propositions. Temporal operators use fixpoints.

Theorem. The set of states satisfying is the least fixpoint of the equation , where are the states where holds and the states with at least one successor in ; it is obtained by iterating , until nothing changes.

Proof. By induction, is the set of states from which is reached in at most steps: it holds for , and a state reaches in at most steps if it is already in or has a successor that gets there in at most . The sequence is increasing and the states are finite, so it stabilises after at most steps, on the set of states from which is reachable in any number of steps: exactly . Every other fixpoint contains and is closed under , so it contains all the : this is the least one. ∎

The other operators reduce to these: ; is the greatest fixpoint of ; . The cost is linear in the number of states and transitions.

State explosion. The problem is that states grow exponentially with the variables: 20 Boolean variables give a million states, 300 give more than the atoms in the universe. NuSMV uses two remedies: symbolic model checking, which represents sets of states as Boolean formulas compressed with BDDs (binary decision diagrams), and bounded model checking, which looks for counterexamples of limited length by turning the problem into a formula for a SAT solver.

An example: mutual exclusion

Two processes share a resource (a printer, a variable) and must never be together in the critical section. Each process has a flag it raises when it wants to enter. A scheduler chooses at each instant which process takes a step: the model’s variable represents this choice, left free (nondeterministic) so that NuSMV examines every possible interleaving.

The naive protocol. Each process checks that the other’s flag is down, then raises its own and enters. It looks correct, but NuSMV answers that the property is false and shows a 6-step counterexample: process 1 checks (the other’s flag is down), then the scheduler lets process 2 check too (the first one’s flag is still down), and both enter. The flaw is that “check” and “raise the flag” are two separate steps.

Peterson’s algorithm (1981) adds a turn variable: each process raises its flag, then gives the turn to the other, and waits until the other does not want to enter or the turn is its own. NuSMV verifies that:

• is true: mutual exclusion is guaranteed;
• is true, and so is the equivalent LTL formula : whoever waits eventually enters;
• the reachable states are 68 out of 400 possible ones.

The importance of fairness. The second property holds only with the clauses FAIRNESS s = 1 and FAIRNESS s = 2, which consider only the executions in which the scheduler lets each process move infinitely often. Removing them, NuSMV finds a counterexample: process 1 waits, and the scheduler moves only process 2 forever, which stays idle. This is not a flaw of the protocol but of the scheduler model: model checking forces these assumptions to be made explicit too.

An application: verifying a website

The same ideas apply to objects very different from a protocol. In the degree thesis from which this topic was born (Politecnico di Bari, 2002) a website is automatically turned into a NuSMV model, and the properties a good site should have are written in CTL. The program developed, DaWeb, reads the pages, builds the model and runs the model checker.

The idea is to view the site as a state machine: the variable Paging tells which page the visitor is on, the variable State tells whether a page is being viewed (page) or a link is being followed (link). Each link on the page is a possible transition; the choice is nondeterministic, because the visitor can click any link. The typical properties of the thesis are:

• reachability of the home page: from every page one can go back to the index, AG (State = page -> EF Paging = index);
• link consistency: every link leads to an existing page, AG (State = link -> EX State = page);
• path constraints: for example, in an online shop, payment is reached only through the login;
• properties of the page content (internal or external pages, static or dynamic, maximum size, update date), verified in the same way with additional variables.

Here is a small online shop in the style of the thesis, with two errors put in on purpose: the product page has a link to offers, which does not exist, and the order confirmation page has no links.

MODULE main
VAR
  State  : {page, link};
  Paging : {index, catalogue, product, cart, login, payment, confirmation, contacts, offers};
ASSIGN
  init(State)  := page;
  init(Paging) := index;
  next(State) := case
    State = page : link;                                 -- a link is clicked
    State = link & Paging = offers : link;               -- missing page: stuck on the link
    TRUE : page;                                         -- the link leads to an existing page
  esac;
  next(Paging) := case
    State = link : Paging;                               -- at the destination the page does not change
    Paging = index        : {catalogue, contacts, login};
    Paging = catalogue    : {product, index};
    Paging = product      : {cart, catalogue, offers};   -- offers does not exist: broken link
    Paging = cart         : {login, catalogue};
    Paging = login        : {payment, index};
    Paging = payment      : {confirmation, cart};
    Paging = confirmation : confirmation;                -- page without links
    Paging = contacts     : index;
    TRUE : Paging;
  esac;
SPEC AG (State = page -> EF (State = page & Paging = index))
SPEC AG (State = link -> EX (State = page))
SPEC AG (Paging = cart -> !E [ !(Paging = login) U (Paging = payment) ])

NuSMV finds both errors and explains them with a counterexample:

• the first property is false: the counterexample is the path index, login, payment, confirmation; from the confirmation page there is no way back to the home page;
• the second is false: the path index, catalogue, product, offers reaches a link that leads to no page;
• the third is true: from the cart there is no path reaching payment without going through the login.

The advantage over a simple program that checks links one by one is that the properties concern paths and not single pages: “after the cart one always goes through the login” cannot be checked by looking at one page at a time. For dynamic sites the thesis adds parameters (for example the logged-in user) and verifies the properties for each value.

Model checking in practice

Model checking is used in digital circuit design (after the famous Pentium division bug in 1994, Intel adopted formal verification systematically for arithmetic units and cache protocols), in communication protocols, in on-board software for aircraft and trains and in industrial control systems. Edmund Clarke, Allen Emerson and Joseph Sifakis received the Turing Award in 2007 for inventing it. The limits are state explosion and the need for a faithful finite model: one verifies the model, not the real code, unless tools that extract the model from the code are used.

Summary

• Model checking explores all reachable states of a finite system and verifies temporal logic properties, returning a counterexample when they are false.
• CTL quantifies over paths (A, E) and over time (X, F, G, U); LTL evaluates formulas on every path.
• The algorithm computes sets of states with fixpoints: least for EF and EU, greatest for EG.
• NuSMV represents sets of states with BDDs and looks for counterexamples with bounded model checking.
• In the example the naive protocol violates mutual exclusion in 6 steps; Peterson’s is safe and live, under the assumption of a fair scheduler.
• The same method verifies a website: pages and links become states and transitions, and NuSMV finds broken links, dead-end pages and forbidden paths.

The full thesis, with the DaWeb program, the site models and all the specifications, can be read here: full thesis (PDF, Italian).

The code

Peterson’s model for NuSMV (file peterson.smv). It is checked with NuSMV peterson.smv; the naive model is the same, with the states idle, check, setf, crit and without the turn variable.

-- Peterson's algorithm: "I want to enter" flag and turn variable t
MODULE main
VAR
  pc1 : {idle, flag, turn, wait, crit};
  pc2 : {idle, flag, turn, wait, crit};
  f1 : boolean;
  f2 : boolean;
  t : {1, 2};
  s : {1, 2};                       -- the process that takes a step at this instant
ASSIGN
  init(pc1) := idle;  init(pc2) := idle;
  init(f1) := FALSE;  init(f2) := FALSE;  init(t) := 1;
  next(pc1) := case
    s = 1 & pc1 = idle : {idle, flag};
    s = 1 & pc1 = flag : turn;
    s = 1 & pc1 = turn : wait;
    s = 1 & pc1 = wait & (!f2 | t = 1) : crit;
    s = 1 & pc1 = crit : idle;
    TRUE : pc1;
  esac;
  next(f1) := case
    s = 1 & pc1 = flag : TRUE;
    s = 1 & pc1 = crit : FALSE;
    TRUE : f1;
  esac;
  next(pc2) := case
    s = 2 & pc2 = idle : {idle, flag};
    s = 2 & pc2 = flag : turn;
    s = 2 & pc2 = turn : wait;
    s = 2 & pc2 = wait & (!f1 | t = 2) : crit;
    s = 2 & pc2 = crit : idle;
    TRUE : pc2;
  esac;
  next(f2) := case
    s = 2 & pc2 = flag : TRUE;
    s = 2 & pc2 = crit : FALSE;
    TRUE : f2;
  esac;
  next(t) := case
    s = 1 & pc1 = turn : 2;         -- give the turn to the other
    s = 2 & pc2 = turn : 1;
    TRUE : t;
  esac;
FAIRNESS s = 1
FAIRNESS s = 2
SPEC AG !(pc1 = crit & pc2 = crit)
SPEC AG (pc1 = wait -> AF pc1 = crit)
LTLSPEC G (pc1 = wait -> F pc1 = crit)

NuSMV’s output:

-- specification AG !(pc1 = crit & pc2 = crit)  is true
-- specification AG (pc1 = wait -> AF pc1 = crit)  is true
-- specification  G (pc1 = wait ->  F pc1 = crit)  is true

The same algorithm in Python, with the states explored one by one (explicit-state model checking): breadth-first search of the reachable states, search for the shortest counterexample and computation of as a least fixpoint.

from collections import deque

# Explicit-state model checking: the same two NuSMV models, states as tuples (pc1, pc2, f1, f2, t, s)

def step_peterson(st, i):
    """Moves of process i (1 or 2) in state st; returns the possible next (pc_i, f_i, t)."""
    pc, f, t = st[i - 1], st[1 + i], st[4]
    other_f, me, other = st[4 - i], i, 3 - i
    if pc == "idle":
        return [("idle", f, t), ("flag", f, t)]
    if pc == "flag":
        return [("turn", True, t)]
    if pc == "turn":
        return [("wait", f, other)]
    if pc == "wait":
        return [("crit", f, t)] if (not other_f or t == me) else [("wait", f, t)]
    return [("idle", False, t)]                      # crit: leaves and lowers its flag


def step_naive(st, i):
    pc, f, t = st[i - 1], st[1 + i], st[4]
    other_f = st[4 - i]
    if pc == "idle":
        return [("idle", f, t), ("check", f, t)]
    if pc == "check":
        return [("setf", f, t)] if not other_f else [("check", f, t)]
    if pc == "setf":
        return [("crit", True, t)]
    return [("idle", False, t)]


def successors(st, step):
    s = st[5]                                        # the process that moves now
    out = []
    for pc, f, t in step(st, s):
        new = list(st)
        new[s - 1], new[1 + s], new[4] = pc, f, t
        for s_next in (1, 2):                        # the next process is chosen nondeterministically
            new[5] = s_next
            out.append(tuple(new))
    return out


def explore(step):
    init = [("idle", "idle", False, False, 1, s) for s in (1, 2)]
    parent = {x: None for x in init}
    queue = deque(init)
    while queue:                                     # breadth-first search: the first bad state found has the shortest path
        x = queue.popleft()
        for y in successors(x, step):
            if y not in parent:
                parent[y] = x
                queue.append(y)
    return parent


def EF(states, step, goal):
    """Set of states from which goal can be reached: least fixpoint Z = goal ∪ pre(Z)."""
    Z = {x for x in states if goal(x)}
    while True:
        new = Z | {x for x in states if any(y in Z for y in successors(x, step))}
        if new == Z:
            return Z
        Z = new


bad = lambda x: x[0] == "crit" and x[1] == "crit"
for name, step in (("naive", step_naive), ("Peterson", step_peterson)):
    parent = explore(step)
    states = set(parent)
    viol = [x for x in states if bad(x)]
    print(f"{name}: {len(states)} reachable states; AG !(crit1 & crit2) {'false' if viol else 'true'}")
    if viol:
        x, path = viol[0], []
        while x is not None:
            path.append(x); x = parent[x]
        print("  counterexample of", len(path) - 1, "steps:", " -> ".join(f"{p[0]}/{p[1]}" for p in reversed(path)))
    good_init = all(x not in EF(states, step, bad) for x in states if x[:5] == ("idle", "idle", False, False, 1))
    print("  initial states outside EF(crit1 & crit2):", good_init)

Running it prints for the naive protocol 32 reachable states, the property false and the 6-step counterexample idle/idle, check/idle, setf/idle, setf/check, setf/setf, crit/setf, crit/crit; for Peterson 68 reachable states, as in NuSMV, and the property true, with the initial state outside the set .