Spin is a model checker for the verification of software systems. Spin uses a high level language called Promela to specify systems descriptions. The goal of this tutorial is to introduce novice users to both Promela and Spin. The tutorial
itself is divided into two parts. The Basic Spin part is targeted towards novice users of Spin. The Advanced Spin part of the tutorial could also be of considerable interest to intermediate Spin users.