Tool Seminar:SPIN Overview

From Dependability

Overview | Schedule | Syllabus | 2006 Project Guidelines | Tool List | Editing Guidelines

 

 

On Wednesday, March 15, we will discuss the SPIN model checker.

SPIN is distributed freely in source form. http://spinroot.com/spin/whatispin.html


An early overview paper of SPIN, with verification examples, is:

link "The Model Checker Spin" by Gerard J. Holzmann

We will not discuss much of the details of the algorithms that SPIN adopts (as in Section 3). However, I will add some comments on the techniques that supported by the newer version of SPIN (e.g. model extraction).


For the application of SPIN, and for particular interest of the group, you can also take a look at its application to the legacy flight software from NASA's Deep Space One (DS1) mission.

link "Using Spin Model Checking for Flight Software Verification" by P.R. Gluck and G.J. Holzmann
Retrieved from "http://dependability.cs.virginia.edu/info/Tool_Seminar:SPIN_Overview"