SPIN is an automated verification tool (model checker), using PROMELA (PROcess MEta LAnguage), a language loosely based on CSP, for finite state systems, such as protocols or validation models of distributed systems, developed at Bell Laboratories.
The complete description of the software.
Add "/soft/lus/spin/bin" to your search path before running the
tool:
setenv PATH {$PATH}:/soft/lus/spin/bin
Invoke the program by typing xspin