For the lecture Advanced Software Quality at Aalen University, I had to demonstrate the usage of Spin model checker for the verification of software models. iSpin represents a graphical interface for editing and executing models and for analyzing the results. iSpin invokes Spin commands in the background and graphically presents the results.

Following these steps, I managed to run Spin model checker on Ubuntu:

  1. Download the Spin binary from Github and extract it to your favorite installation directory:
    tar xfz version-6.5.2.tar.gz
  2. Build the Spin binary:
    sudo apt-get install -y build-essential byacc flex graphviz
    cd $INSTALL_DIR/Spin-version-*/Src
    sudo cp spin /usr/bin/
  3. This is how you can execute a simple model written in Promela, the modeling language for Spin, from the command line:
    spin $INSTALL_DIR/Spin-version-*/Examples/hello.pml
  4. The usage of iSpin requires the installation of tk, a graphical user interface toolkit:
    sudo apt-get install -y tk
    cd $INSTALL_DIR/Spin-version-*/optional_gui/