Testing

SPIN and NuSMV: Model Checkers for Concurrent System Verification

09 Oct 2026 — 6 min read

Race conditions are one of the hardest bugs to find with tests. A threading bug might only trigger after a specific interleaving of 8 operations across 3 goroutines, and the window for that interleaving might be 10 nanoseconds. You could run the test a million times and never hit it — until production.

Model checkers for concurrent systems take a different approach: instead of running the program, they exhaustively explore all possible execution orderings. SPIN and NuSMV are two mature, widely-used model checkers that can find concurrency bugs, protocol violations, and state machine errors that would take months of testing to stumble upon.

SPIN: Concurrent Systems Model Checking

SPIN (Simple Promela Interpreter) is the most widely used explicit-state model checker. It verifies models written in Promela (Process Meta Language), an executable specification language for concurrent systems.

SPIN was developed at Bell Labs, won the ACM Software System Award in 2001, and has been used to verify protocols in NASA space missions, network protocols, and concurrent algorithms.

Installing SPIN

# macOS
brew install spin

# Ubuntu
apt install spin

# Or build from source
wget https://spinroot.com/spin/Src/spin649.tar.gz
tar xzf spin649.tar.gz
cd Spin/
make
sudo mv spin /usr/local/bin/

Promela: Concurrent Processes

Promela models concurrent processes communicating via channels:

/* Simple producer-consumer with a buffer of size 1 */

mtype = { ITEM };

chan buffer = [1] of { mtype };

bool produced = false;
bool consumed = false;

active proctype Producer() {
    buffer ! ITEM;
    produced = true;
}

active proctype Consumer() {
    mtype item;
    buffer ? item;
    consumed = true;
}

/* LTL property: eventually both produced and consumed */
ltl correctness { <> (produced && consumed) }

Run SPIN:

# Verify LTL property
spin -a model.pml
gcc -o pan pan.c
./pan -a  # check all acceptance cycles

# Simulate (random execution)
spin -p -u 100 model.pml

Modeling a Mutex Protocol

/* Peterson's mutual exclusion algorithm */

bool flag[2] = false;
int turn = 0;
bool critical[2] = false;

/* Safety: at most one in critical section */
#define mutex (!(critical[0] && critical[1]))

active [2] proctype Process()
{
    int i = _pid;   /* 0 or 1 */
    int j = 1 - i;  /* the other process */
    
    do
    ::  /* Entry protocol */
        flag[i] = true;
        turn = j;
        
        /* Wait until it's safe to enter */
        (flag[j] == false || turn == i);
        
        /* Critical section */
        critical[i] = true;
        assert(mutex);  /* safety check */
        critical[i] = false;
        
        /* Exit protocol */
        flag[i] = false;
    od;
}

ltl mutual_exclusion { [] mutex }
ltl no_starvation { 
    [] (flag[0] -> <> critical[0]) &&
    [] (flag[1] -> <> critical[1])
}

SPIN verifies mutual_exclusion — that both processes are never in the critical section simultaneously — by exploring every possible interleaving.

LTL Properties in SPIN

Linear Temporal Logic (LTL) operators in SPIN:

Operator	Meaning	Promela Syntax
`[] P`	Always P	`[] P`
`<> P`	Eventually P	`<> P`
`P U Q`	P until Q	`P U Q`
`P -> Q`	P implies Q	`P -> Q`

Common patterns:

/* Safety: bad state never reached */
ltl safety { [] !bad_state }

/* Liveness: request always eventually granted */
ltl liveness { [] (request -> <> granted) }

/* No starvation: process always eventually runs */
ltl no_starvation { [] <> running }

/* Bounded response: response within 3 steps */
ltl bounded { [] (req -> (granted || X (granted || X granted))) }

Channel Communication and Deadlock Detection

/* Dining philosophers — check for deadlock */

#define N 5

chan fork[N] = [1] of { bool };

init {
    int i;
    for (i : 0 .. N-1) {
        fork[i] ! true;
    }
}

active [N] proctype Philosopher()
{
    int left = _pid;
    int right = (_pid + 1) % N;
    bool f;
    
    do
    ::  /* Pick up left fork */
        fork[left] ? f;
        /* Pick up right fork */
        fork[right] ? f;
        /* Eat */
        /* Put down forks */
        fork[right] ! true;
        fork[left] ! true;
    od;
}

/* SPIN will find the deadlock automatically — no ltl needed */
/* All philosophers hold left fork, wait for right */

Run with deadlock detection:

./pan -d  # detect deadlocks

SPIN produces a counterexample trace showing the exact sequence of steps leading to deadlock.

Partial Order Reduction

For large models, SPIN's state space explodes. Partial order reduction (POR) prunes equivalent interleavings:

# Enable POR (default in most versions)
./pan -p  # full POR

# BitState hashing for very large state spaces
./pan -DBITSTATE  # compile with bitstate

Supertrace (bitstate) sacrifices completeness for scalability — useful when you need to check large real-world protocols.

NuSMV: Symbolic Model Checking

NuSMV uses BDD-based (Binary Decision Diagram) symbolic model checking, which handles much larger state spaces than SPIN's explicit-state approach. It's especially effective for hardware designs and controllers.

Installing NuSMV

# macOS
brew install nusmv

# Ubuntu — usually needs manual install
wget https://nusmv.fbk.eu/NuSMV/download/getting-v2/NuSMV-2.6.0-linux64.tar.gz
tar xzf NuSMV-2.6.0-linux64.tar.gz

# Or use NuXMV (successor)
# https://nuxmv.fbk.eu/

NuSMV Modules and State Machines

NuSMV models are state machines with explicit initial states and transition relations:

-- Traffic light controller

MODULE main
VAR
    light : {red, yellow, green};
    timer : 0..30;

ASSIGN
    init(light) := red;
    init(timer) := 0;
    
    next(light) :=
        case
            light = red    & timer >= 30 : green;
            light = green  & timer >= 25 : yellow;
            light = yellow & timer >= 5  : red;
            TRUE                         : light;
        esac;
    
    next(timer) :=
        case
            next(light) != light : 0;
            TRUE                 : min(timer + 1, 30);
        esac;

-- Safety: never directly green to red
LTLSPEC G (light = green -> X(light != red))

-- Liveness: green light eventually reached
LTLSPEC F (light = green)

Run NuSMV:

NuSMV traffic.smv

Output:

-- specification G (light = green -> X light != red)  is true
-- specification F (light = green)  is true

CTL vs LTL in NuSMV

NuSMV supports both CTL (Computation Tree Logic) and LTL. CTL reasons about branching time:

CTL Operator	Meaning
`EX P`	There exists a next state where P
`AX P`	All next states satisfy P
`EF P`	There exists a path where P eventually holds
`AF P`	All paths: P eventually holds
`EG P`	There exists a path where P always holds
`AG P`	All paths: P always holds
`E[P U Q]`	Some path: P until Q
`A[P U Q]`	All paths: P until Q

-- CTL properties
CTLSPEC AG (light = red -> EF(light = green))   -- always possible to reach green from red
CTLSPEC AG !(light = red & light = green)        -- never red AND green simultaneously

-- LTL properties  
LTLSPEC G (light = red -> F light = green)       -- always eventually green after red
LTLSPEC G (light = green -> !X(light = red))     -- no direct green->red transition

Modeling a Protocol with NuSMV

Two-phase commit protocol:

MODULE coordinator(votes)
VAR
    state : {INIT, WAIT, COMMIT, ABORT};
    
ASSIGN
    init(state) := INIT;
    
    next(state) :=
        case
            state = INIT                          : WAIT;
            state = WAIT & votes = all_yes        : COMMIT;
            state = WAIT & votes != all_yes       : ABORT;
            TRUE                                  : state;
        esac;

MODULE participant(coordinator_decision)
VAR
    state : {READY, COMMITTED, ABORTED};
    
ASSIGN
    init(state) := READY;
    
    next(state) :=
        case
            state = READY & coordinator_decision = COMMIT : COMMITTED;
            state = READY & coordinator_decision = ABORT  : ABORTED;
            TRUE                                           : state;
        esac;

MODULE main
VAR
    votes    : {all_yes, some_no};
    coord    : coordinator(votes);
    part1    : participant(coord.state);
    part2    : participant(coord.state);

-- Agreement: both participants make the same decision
CTLSPEC AG (part1.state = COMMITTED -> part2.state = COMMITTED)
CTLSPEC AG (part1.state = ABORTED   -> part2.state = ABORTED)

-- Termination: coordinator eventually decides
CTLSPEC AF (coord.state = COMMIT | coord.state = ABORT)

Counterexample Analysis in NuSMV

When NuSMV finds a property violation, it produces a counterexample trace:

-- specification AG (...) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    votes = all_yes
    coord.state = INIT
    part1.state = READY
  -> State: 1.2 <-
    coord.state = WAIT
  -> State: 1.3 <-
    votes = some_no    <-- non-deterministic choice
    coord.state = ABORT
  -> State: 1.4 <-
    part1.state = ABORTED
    part2.state = COMMITTED    <-- VIOLATION: inconsistent decisions

The counterexample shows that when votes changes non-deterministically between the coordinator's decision states, participants can reach different conclusions.

CI Integration

# .github/workflows/model-check.yaml
name: Model Checking
on:
  push:
    paths:
      - 'models/**/*.pml'
      - 'models/**/*.smv'

jobs:
  spin:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - run: apt-get install -y spin
      - name: Check Promela models
        run: |
          for f in models/**/*.pml; do
            spin -a "$f"
            gcc -o pan pan.c
            ./pan -a || (echo "SPIN violation in $f"; exit 1)
          done
  
  nusmv:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install NuSMV
        run: |
          wget -q https://nusmv.fbk.eu/NuSMV/download/getting-v2/NuSMV-2.6.0-linux64.tar.gz
          tar xzf NuSMV-2.6.0-linux64.tar.gz
          echo "$PWD/NuSMV-2.6.0-linux64/bin" >> $GITHUB_PATH
      - name: Check SMV models
        run: |
          for f in models/**/*.smv; do
            NuSMV "$f" | grep -E "^-- specification" | grep -v "is true" && exit 1 || true
          done

Choosing Between SPIN and NuSMV

Use SPIN when:

Verifying concurrent software protocols (Go channels, POSIX threads, message passing)
You want to write executable specifications (Promela can be simulated)
State space is small to medium (explicit state)
You need LTL liveness checking

Use NuSMV when:

Verifying hardware controllers or state machines
State space is large (BDD symbolic checking handles it better)
You want CTL branching-time properties
You're verifying reactive systems

For distributed systems software, SPIN is usually the better fit. For embedded controllers and hardware models, NuSMV or its successor NuXMV.