ABSTRACT
Model checking is a widespread formal verification technique aimed at evaluating the properties of a complex system. In recent years, the general approach of model checking has been applied to a broad spectrum of application areas, ranging from hardware components design to software and system engineering. Like virtually all other model checkers, Spin requires and works on a model of the system under analysis and a property to be verified, both specified by means of a suitable formal language. Informally speaking, Spin aims at proving that the property of interest holds by systematically exploring every possible state the system under analysis can reach during its execution, starting from its initial or starting state. Starting from a model, Spin can perform two different activities: simulate the system behavior in various ways and verify whether or not a property holds by means of state space exploration. Most often, Spin is not invoked directly by the user, but through a graphical front end.
