Sunday, April 20, 2008

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!


Anonymous said...

Just so you know, Spin tends to leave dead processes that influence the results of the verification. I lost a whole afternoon trying to figure out some errors in my code that weren't really there, they were the result of Spin not cleaning up properly.

Every once in a while shut down Spin, and manually kill any "spin" processes that were left over, and restart spin.

Good luck with verifying :-)

Anoj said...

thanks for the tip. Glad to see there are some spin users in the community ;)