Principles of the Spin
Model Checker
Book Cover Image
This is an introductory textbook on the use of the Spin Model Checker for modeling and verifying concurrent and distributed systems.
- Foreward, preface and table of contents.
- Supplementary material on version 6 of Spin.
-
Source code of the Promela programs in the book.
The Promela programs have been adapted to use the new features of version 6 of Spin; "-6" has been added to their file names to distinguish them from the original programs that are still in the archive. - Source code of the Promela programs in the book adapted for use with the Erigone Model Checker.
- Slides (PDF and LaTeX).
- Errata (last update 24 August 2008).
- Spin reference card (PDF and LaTeX).
Tools for learning model checking and Spin:
- jSpin: An integrated development environment.
- Erigone: A reimplementation of Spin for facilitating learning.
Japanese translation
published by Ohmsha