How to install spin model checker on Linux ubuntu 16.04

This tutorials explains, how to install Spin on Linux Ubuntu 16.04. Spin is  Logic model checking and in the formal verification of concurrent systems and multi-threaded software applications.

The tool supports a high level language to specify systems descriptions called PROMELA (short for: PROcess MEta LAnguage)  and provides direct support for the use of embedded C code as part of model specifications. Spin can be used as as a simulator , as an exhaustive verifier , as proof approximation system & as a driver for swarm verification. All Spin software is written in C language  and it is portable across all Platforms as Windows, Linux, Mac.

To install Spin on Linux Ubuntu 16.04

download  recent .tar-file with sources of Spin software from this link ( download Spin Software).

Update & Install Essentials Components.

sudo apt-get update

sudo apt-get install build-essential

Copy spin packed file to opt folder

cp spin*.tar.gz  /opt/

cd /opt/

Extract spin using following command

tar -zxvf  spin*.tar.gz

Goto Spin Folder

cd  spin*/Spin

Goto Source Folder

cd  Src*

Compile Source files


if you face error , install yacc by following command.

sudo apt-get install byacc flex


if u get output as above, goto examples folder.

cd ..

cd Examples

To Test the installation , Type following command

Examples folders contains various ready example in PROMELA language , u can run any file to test installation.

spin hello.pml

if u get output as

passed first test ! 1 process created.

means u have installed spin correctly.

u can also test graphical user interface to spin, which is ispin

ispin hello.pml

Thanks !

Here is the more Tutorials , Books , Papers & Exercises .