The Spin Model Checker

• Spin is a model checker for communicating concurrent processes. It checks:

  • Safety/termination properties
  • Liveness/deadlock properties
  • Path assertions (requirements/never claims)

• It works on finite models, written the Promela language, which describe infinite executions.

• Explores the entire state space of the model, including all possible concurrent executions, verifying that Bad Things don't happen.

• Not an absolute proof – pretty useful in practice

• Make systems reliable by concentrating complexity in a verifiable component

Notes: