jSpin is a graphical user interface for the Spin model checker that is used for verifying concurrent and distributed programs. The user interface of jSpin is simple and consists of a single window with menus, a toolbar and three adjustable text areas. Spin option strings are automatically supplied and the Spin output is filtered and presented in a tabular form. All aspects of jSpin are configurable: some at compile time, some at initialization through a configuration file and some at runtime.

jSpin includes SpinSpider which generates a graphical representation of the state space during a verification. The feature is not robust and I consider it deprecated. Instead, use the VMC (Visualization of Model Checking) postprocessor for the Erigone Model Checker which generates graphs that show the model checking algorithm incrementally.

Required software

  • jSpin invokes the Spin model checker which is included in the Windows installer, but you may want to download the latest version from the Spin website.
  • A C compiler is needed for running Spin. I suggest MinGW for Windows.


Download from GitHub: https://github.com/motib/jspin.