Spin Model Checker, The: Primer and Reference Manual

Chapter 11. Using SPIN

	“The difference between theory and practice is a lot bigger in practice than in theory.”
	--(Peter van der Linden, Expert C Programming, p. 134)

Although SPIN verifications are often performed most conveniently with the help of the graphical interface XSPIN, we will postpone a discussion of that tool for one more chapter and concentrate here on a bare bones use of SPIN itself. It can be very useful to know how to run short verification jobs manually through SPIN’s command line interface, especially when trying to troubleshoot unexpected results.

The number of industrial applications of SPIN is steadily increasing. The core intended use of the tool, though, has always been to support both research and teaching of formal verification. ...