IEEE TRANSACTIONS ON SOFTWARE ENGINEERING VOL 23 NO 5 MAY 1997 1 The Model Checker SPIN Gerard J Holzmann Abstract SPIN is an efficient verification system for models of distributed software systems It has been used to detect design errors in applications ranging from high level descriptions of distributed algorithms to detailed code for controlling telephone exchanges This paper gives an overview of the design and structure of the verifier reviews its theoretical foundation and gives an overview of significant practical applications Index Terms Formal methods program verification design verification model checking distributed systems concurrency 1 INTRODUCTION S PIN is a generic verification system that supports the design and verification of asynchronous process systems 36 38 SPIN verification models are focused on proving the correctness of process interactions and they attempt to abstract as much as possible from internal sequential computations Process interactions can be specified in SPIN with rendezvous primitives with asynchronous message passing through buffered channels through access to shared variables or with any combination of these In focusing on asynchronous control in software systems rather than synchronous control in hardware systems SPIN distinguishes itself from other well known approaches to model checking e g 12 49 53 As a formal methods tool SPIN aims to provide 1 an intuitive program like notation for specifying design choices unambiguously without implementation detail 2 a powerful concise notation for expressing general correctness requirements and 3 a methodology for establishing the logical consistency of the design choices from 1 and the matching correctness requirements from 2 Many formalisms have been suggested to address the first two items but rarely are the language choices directly related to a basic feasibility requirement for the third item In SPIN the notations are chosen in such a way that the logical consistency of a design can be demonstrated mechanically by the tool SPIN accepts design specifications written in the verification language PROMELA a Process Meta Language 36 and it accepts correctness claims specified in the syntax of standard Linear Temporal Logic LTL 60 There are no general decision procedures for unbounded systems and one could well question the soundness of a design that would assume unbounded growth Models that can be specified in PROMELA are therefore always required G J Holzmann is with the Computing Sciences Research Center Bell Laboratories Murray Hill NJ 07974 Email gerard research bell labs com Manuscript received Sept 30 1996 Recommended for acceptance by L K Dillon and S Sankar For information on obtaining reprints of this article please send e mail to transse computer org and reference IEEECS Log Number 104928 0 to be bounded and have only countably many distinct behaviors This means that all correctness properties automatically become formally decidable within the constraints that are set by problem size and the computational resources that are available to the model checker to render the proofs All verification systems of course do have physical limitations that are set by problem size machine memory size and the maximum runtime that the user is willing or able to endure These constraints are an often neglected issue in formal verification We study the limitations of the model checker explicitly and offer relief strategies for problems that are outside the normal domain of exhaustive proof Such strategies are discussed in Sections 3 3 and 3 4 of this paper 1 1 Structure The basic structure of the SPIN model checker is illustrated in Fig 1 The typical mode of working is to start with the specification of a high level model of a concurrent system or distributed algorithm typically using SPIN s graphical front end XSPIN After fixing syntax errors interactive simulation is performed until basic confidence is gained that the design behaves as intended Then in a third step SPIN is used to generate an optimized on the fly verification program from the high level specification This verifier is compiled with possible compile time choices for the types of reduction algorithms to be used and executed If any counterexamples to the correctness claims are detected these can be fed back into the interactive simulator and inspected in detail to establish and remove their cause The remainder of this paper consists of three main parts Section 2 gives an overview of the basic verification method that SPIN employs Section 3 summarizes the basic algorithms and complexity management techniques that have been implemented Section 4 gives three examples of typical applications of the SPIN model checker to design and verification problems The first example is the problem of devising a correct process scheduler for a distributed operating system the second problem is the verification of a leader election protocol for a distributed ring the third problem is the proof of correctness of a standard sliding window flow control protocol Section 4 concludes with a summary of a range of other significant verification problems to which SPIN has been applied Section 5 concludes the paper 0098 5589 97 10 00 1997 IEEE J PRODUCTION TSE 2 INPROD MAY 104928 0 104928 1 DOC regularpaper97 dot S 27 136 05 29 97 4 13 PM 1 17 2 IEEE TRANSACTIONS ON SOFTWARE ENGINEERING VOL 23 NO 5 MAY 1997 Fig 1 The structure of SPIN simulation and verification 2 FOUNDATION SPIN has its roots in the earliest protocol verification systems based on on the fly reachability analysis from the early 80s 32 33 34 The purpose of these first verifiers was to provide an effective tool that could be used to solve problems of practical significance The fundamental computational complexity of the problem to be solved forces one to choose carefully which features will be supported or risk compromising the practical significance of the tool itself The predecessors of SPIN therefore supported the verification of only standard safety properties and a limited range of liveness properties Work on logic model checking techniques pioneered by Clarke and Emerson 12 and by Sifakis and Queille 61 laid the foundation for a new generation of model checking tools with a larger scope of verification capabilities Vardi and Wolper extended this work with an automata theoretic model 77 that has become the formal basis for temporal logic model checking in the SPIN system The framework is summarized