Spin is a model checker available at www.spinroot.com.

0. Install Spin and iSpin by following the instructions found at:
http://spinroot.com/spin/Man/README.html.

1. Spin is the actual model checker. iSpin is a graphical front end
for Spin.

2. Spin takes Promela files as input. You can load a Promela file in
iSpin and perform simulation and verification of the
model. Alternatively, you can directly use Spin in command line. To
familiarize yourself with Promela and Spin, have a look at:

 - the following examples and exercises: http://spinroot.com/spin/Man/Exercises.html,
 - the Spin manual: http://spinroot.com/spin/Man/Manual.html,
 - the Promela manual: http://spinroot.com/spin/Man/promela.html.