Materials

Book

There is no mandatory book used in the course, but the following book is highly recommended if you to want learn more about Spin or use its more advanced features. It focuses on how Spin is used, rather than how Spin works. The book store can get it home in a few days.

"Principles of the Spin Model Checker", Ben-Ari, Mordechai
2008, XVI, 216 p. 17 illus., Softcover
ISBN: 978-1-84628-769-5

Literature/articles/notes


Reference/link
Description
[1]
“A Primer on Model Checking”, Mordechai Ben-Ari, article from ACM Inroads, March 2010.
[2]
“Basic Spin Manual” from the Spin homepage http://spinroot.com
[3]
“Consistent Global States of Distributed Systems: Fundamental Concepts and Mechanisms”, Technical Report UBLCS-93-1, January 1993, University of Bologna
[4]
Guide for installing jSpin + Spin in newest version.


Promela demo programs

tds1.pml - Two processes updating the same counter.
tds2.pml - Two processes going into deadlock.
count-6.pml - Surprising interference with 2 processes incrementing a counter.
tds3.pml - Simple client/server system.
fairness.pml - Illustrates difference between minimal fairness and weak fairness.

Additional information on Spin

The Spin Cheat Sheet provides a short, reference-like description of the most important parts of Spin.