Running SPIN (Promela Model Checking) on linux

Continuing on from my posts on running academic tools on linux, here I'll show you how to run SPIN on Linux. For those interested in SPIN, SPIN is an interpreter for Promela (Process Meta Language) and is used for verifying the correctness of distributed software (software design) in a rigorous and mostly automated fashion. If you have done any courses on parallel and concurrent programming or on Distributed systems, you would have definitely heard of Spin and SMV. Here are the steps..

1. Download 2 files - Latest Spin binary and Xspin from the spin website.

2. Install tk8.4 via synaptic or apt
$ sudo apt-get install tk8.4

3. Move/Copy the downloaded spin binary to "/usr/bin" folder
$ sudo cp spin514_linux /usr/bin/spin

4. Run Xspin binary
$ wish xspin430.tcl

Happy Learning!

Linux: Installing Cadence SMV for Model Checking

This post is for all those computer science students who have to face the pain of doing Model checking and verification course as a part of their graduation requirements. One of the most common tool kits used for this purpose is the Cadence Berkley SMV
Get the linux binary package from here

Here are the steps to install it:

1. Extract the tar file to some folder called smv. Change to that folder and copy it to /usr/local

$sudo cp -r smv /usr/local/

2. Set path variables and links

$sudo export PATH=$PATH:/usr/local/smv/bin

$sudo ln -s /usr/local/smv/lib/ /usr/lib/

$sudo ln -s /usr/local/smv/lib/ /usr/lib/

3. The command line smv program should start working now. Type this and test


4. To get the gui version - vw running, we need to install some additional packages. Fire up synaptics and install these 2 packages.
tk8.4 8.4.15-1ubuntu1

4. vw can be run now. Run this and test


PS: To run it as a normal user, you can either add the path of smv bin to profile $PATH
$sudo ln -s /usr/local/smv/bin/smv /usr/bin/smv
$sudo ln -s /usr/local/smv/bin/vw /usr/bin/vw
$sudo chmod u+x smv
$sudo chmod u+x vw