spin2004-ruys-holzmann-tutorial

Advanced SPIN Tutorial1 2Theo C. Ruys and Gerard J. Holzmann1 Department of Computer Science, University of Twente.P.O. Box 217, 7500 AE Enschede, The Netherlands.http://www.cs.utwente.nl/~ruys/2 NASA/JPL, Laboratory for Reliable Software.4800 Oak Grove Drive, Pasadena, CA 91109, USA.http://spinroot.com/gerard/Abstract. Spin [9] is a model checker for the veri cation of distributedsystems software. The tool is freely distributed, and often described asone of the most widely used veri cation systems. The Advanced Spin Tu-torial is a sequel to [7] and is targeted towards intermediate to advancedSpin users.1 IntroductionSpin [2{5, 9] supports the formal veri cation of distributed systems code. Thesoftware was developed at Bell Labs in the formal methods and veri cation groupstarting in 1980. Spin is freely distributed, and often described as one of the mostwidely used veri cation systems. It is estimated that between 5,000 and 10,000people routinely use Spin. Spin was awarded the ACM Software System Awardfor 2001 [1].The automata-theoretic foundation for Spin is laid by [10]. The very recent[5] describes Spin 4.0, the latest version of the tool.The Spin software is written in standard ANSI C, and is portable acrossall versions of the UNIX operating system, including Mac OS X. It can also becompiled to run on any standard PC running Linux or Microsoft Windows.2 TutorialThe Advanced Spin Tutorial is a sequel to [7] and is targeted towards ...