This is a quick cheat sheet for the various model checkers that I come into contact with. It is by no means exhaustive and might be added to later. I regularly found myself looking up this information to remind myself which model-checkers do what and using which languages to describe their models and specify their properties. Writing it down in one place seemed like a good idea.

What is Model Checking?

Model checking is a technique for verifying is a system is a model for a formula; that is, the system has whatever property the formula describes. Model-Checking tools verify that a system exhibits a property by exhaustively exploring that system. This means that model-checking generally requires finite-state systems and large numbers of states can make the problem intractable. However, automatic verification without having to write proofs can be very beneficial. Model-Checking is, relatively, quick; it can expose concurrency bugs, which are difficult to find by testing; and they produce a counterexample, a chain of behaviour that leads to a state that doesn’t exhibit the property, which is invaluable for debugging.

Model-Checking Tools

This table shows a quick summary of the model-checking tools, the languages used to describe the models, and the languages used to specify their properties.

Tool Model Language Property Language
NuSMV Binary Decision Diagrams LTL or CTL
SPIN Promela LTL
PRISM Markov chains or probabilistic timed automata Custom language subsuming various probabilistic temporal logics
UPPAAL Timed automata variants of TCTL and MITL
FDR CSPm CSPm
ProB/ProZ B or Z LTL
Java Pathfinder Java Java

NuSMV

NuSMV is a reimplementation of SMV model checker using temporal logics.

  • Model Language: Binary Decision Diagrams
  • Property Language(S): Linear-Time Temporal Logic or Computation Tree Logic
  • NuSMV2 adds SAT-based model checking
  • Text-based interface
    • Interactive, and;
    • Batch

SPIN

SPIN stands for “Simple Promela Interpreter”, using temporal logics.

  • Model language: Promela (Pro cess Me ta La guage)
    • Asynchronous non-deterministic automata
    • Loosely based on Dijkstra’s guarded command language
    • Borrows I/O operations from CSP
  • Property Language: Linear Temporal Logic (LTL)
  • Designed for multi-threaded software
  • Dynamic number of processes

PRISM

PRISM is a probabilistic (and temporal logic) model checker.

  • Model language(s): PRISM modelling language, which captures:
    • Discrete-time Markov chains,
    • Continuous-time Markov chains,
    • Markov decision processes, and,
    • Probabilistic extensions of the timed automata formalism
  • Property Language: PRISM’s property specification language
    • Subsumes several Probabilistic temporal logics: including PCTL, CSL, probabilistic LTL and PCTL*
    • textual language, based on guarded commands
  • Used for checking stochastic and temporal behaviour

UPPAAL

UPPAAL is a tool for Real-Time Systems model checking using temporal logic.

  • Model Language: networks of Timed Automata
  • Property Language:
    • A simplified form of Timed TCTL (for standard model checking queries – i.e. reachability, invariance, inevitability and leads-to )
    • A weighted extension of Metric Interval Temporal Logic (for Statistical Model Checking)

FDR

FDR stands for Failures Divergences Refinement. it is the model checker for CSP.

  • Model language: CSPm (machine-readable CSP)
  • CSP process algebra, and tockCSP sections. Also has some formal programming concepts thrown in.
  • Really a refinement checker, to the properties are specified in CSP as well
    • Also includes basic checks for deadlock, divergence, and non-determinism
  • Also includes Probe
    • CSPm animator
    • Used to be separate, but now nicely integrated

ProB/ProZ

ProB/ProZ is a model checker for B (and Z) notations.

  • Model language(s): B or Z specifications; also, Event-B, TLA+, CSPm, Promela
    • Z specifications are converted into B-Machines
  • Essentially for State-Based systems
    • Has been extended for others
  • Property Language: Linear-Time Temporal Logic
  • Checks
    • Invariants
    • Deadlocks
    • Properties in Linear-Time Temporal Logic
  • Also has an animator

Java Pathfinder

Java Pathfinder (JPF) is a program model checker for Java programs. It has a specialised Java Virtual Machine that executes all combinations of threads and paths through a Java program.

  • Model Language: Java
  • Property Language: Java
    • Set of defaults: deadlocks and unhandled exceptions
    • Allows writing “little plugins” as Java listeners to monitor JPF execution
  • Not lightweight because it runs on the program