Spin/iSpin Model Checker

Introduction

SPIN is a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.

Usage

Compute Systems Invocation Version(s)
Red Hat Linux (64-bit) % /util/bin/spin 6.4.8 (default)
Red Hat Linux (64-bit) % /util/bin/ispin 1.1.4 (default)

Notes

  1. spin requires input files. You may run spin with sample input files in the Test directory: 

    % spin /util/Spin/Test/hello

  2. ispin is the graphical interface to run spin.

People

  1. Bharat Jayaraman, Instructor.

References

  1. http://en.wikipedia.org/wiki/SPIN_model_checker
  2. http://spinroot.com