This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Model Checker SPIN
May 1997 (vol. 23 no. 5)
pp. 279-295

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.

[1] A. Agarwal, "A Unified Approach to Fault-Tolerance in Communication Protocols, Based on Recovery Procedures," PhD thesis, Computer Science Dept., Concordia Univ., Montreal, Canada, 1995.
[2] M. Alipour, "On the Application of an Automated Validation Tool to Realistic Protocols," MSc thesis, INRS-Telecommunications, Univ. du Quebec, Canada, Aug. 1994.
[3] P.R. D'Argenio, J.P. Katoen, T. Ruys, and J. Tretmans, "Modeling and Verifying a Bounded Retransmission Protocol," Proc. COST 247 Int'l Workshop Applied Formal Methods in System Design,Maribor, Slovenia, June 1996.
[4] A. Basu, M. Hayden, G. Morrisett, and T. von Eicken, "A Language-Based Approach to Protocol Construction," Proc. ACM SIGPLAN Workshop Domain Specific Languages (WDSL),Paris, Jan. 1997.
[5] R. Bharadwaj and C. Hemeyer, "Verifying SCR Requirements Specifications Using State Exploration," Proc. First ACM/SIGPLAN Workshop Automatic Analysis of Software, R. Cleaveland and D. Jackson, eds., pp. 9-24,Paris, Jan. 1997.
[6] B. Boigelot and P. Godefroid, "Model Checking in Practice: An Analysis of the ACCESS Bus Protocol Using SPIN," Proc. Formal Methods Europe (FME96),Oxford, England, Lecture Notes in Computer Science 1,051, pp. 465-478. Springer-Verlag, Mar. 1996.
[7] L. Bouvin, "Design of Validation Models in PROMELA for the Medium, Access Protocol of the PTM Project," Report Royal Inst. of Tech nology, Stockholm, Sweden, Aug. 1991.
[8] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang., "Symbolic model checking: 1020states and beyond," Information and Computation, vol. 98, no. 2, pp. 142-170, June 1992.
[9] T. Cattel, "Modeling and Verification of a Multiprocessor Real-Time OS Kernel," Proc. Seventh Int'l Conf. Formal Description Techniques, pp. 35-50,Berne, Switzerland, Oct. 1994.
[10] T. Cattel, "Using Concurrency and Formal Methods for the Design of Safe Process Control," Proc. PDSE/ICSE018 Workshop,Berlin, Mar. 1996.
[11] J. Chaves, "Formal Methods at AT&T, An Industrial Usage Report," Proc. Fourth FORTE Conf. Formal Description Techniques, pp. 83-90,Sydney, Australia, 1991.
[12] E.M. Clarke and E.A. Emerson, "Synthesis of synchronization skeletons for branching time temporal logic," Logic of Programs: Workshop, Lecture notes in Computer Science. vol. 131. Yorktown Heights, N. Y.: Springer-Verlag, May 1981.
[13] C-T. Chou and D. Peled, "Verifying a Model-Checking Algorithm," Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS96),Passau, Germany, Lecture Notes in Computer Science 1,055, pp. 241-257. Springer-Verlag, Mar. 1996.
[14] Y. Choueka, "Theories of Automata on Mega-Tapes: A Simplified Approach," J. Computer and System Science, vol. 8, pp. 117-141, 1974.
[15] A. Cimatti, A. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, and P. Traverso, "Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System," Proc. Third SPINWorkshop, R. Langerak, ed., Twente Univ., The Netherlands, Apr. 1997.
[16] J.C. Corbett, “Evaluating Deadlock Detection Methods for Concurrent Software,” IEEE Trans. Software Eng., vol. 22, no. 3, pp. 161–179, Mar. 1996.
[17] C. Courcoubetis, M.Y. Vardi, P. Wolper, M. Yannakakis, "Memory Efficient Algorithms for the Verification of Temporal Properties," Formal Methods in Systems Design, vol. I, pp. 275-288, 1992.
[18] D. Dolev, M. Klawe, and M. Rodeh, "An O(n log n) Unidirectional Distributed Algorithm for Extrema Finding in a Circle," J. Algorithms, vol. 3, pp. 245-260, 1982.
[19] G. Duval and J. Julliand, "Modeling and Verification of the RUBIS Micro-Kernel with SPIN," Proc. First SPINWorkshop, J.-Ch. Gregoire, ed., INRS Quebec, Canada, Oct. 1995.
[20] P. Van Eijk, "Verifying Relay Circus Using State Machines," Proc. Third SPINWorkshop, R. Langerak, ed., Twente Univ., The Netherlands, Apr. 1997.
[21] H. Erdogmus, "Verifying Semantic Relations in SPIN," Proc. First SPINWorkshop, J.-Ch. Gregoire, ed., INRS Quebec, Canada, Oct. 1995.
[22] M.J. Ferguson, "Validation of the Radio Link Protocol," Data Services Task Group of ANSI Accredited TIA TR45-3, Contribution TR45.3.2.5/93.08.25.02, Sept. 1993.
[23] M.J. Ferguson, "Formalization and Validation of the Radio Link Protocol RLP1," Computer Networks and ISDN Systems, to appear, 1997.
[24] F. Gagnon, "Boulier, un validateur pour la language de spécification Gaston," PhD thesis, Univ. de Quebec, Canada, July 1995.
[25] R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18,Warsaw, Poland, Chapman&Hall, June 1995.
[26] P. Godefroid and G.J. Holzmann, "On the Verification of Temporal Properties," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV93), pp. 109-124,Liege, Belgium, North-Holland, June 1993.
[27] P. Godefroid, "Partial Order Methods for the Verification of Concurrent Systems," Lecture Notes in Computer Science 1,032. Springer-Verlag, 1996.
[28] P. Godefroid, "Symbolic Protocol Verification with Queue BDDs," Proc. Logic in Computer Science, pp. 198-206, Rutgers Univ., New Brunswick, N.J., July 1996.
[29] J.-C. Gregoire, "State Space Compression in SPINwith GETSs," Proc. Second SPINWorkshop, Rutgers Univ., New Brunswick, N.J., DIMACS/32, Am. Math. Soc., Aug. 1996.
[30] M. Griffioen, "Specification and Verification of a Wireless LAN Controller Chip Using PROMELAand SPIN," Technical Report, AT&T Network Wireless Systems, The Netherlands, 1996.
[31] J. Hajek, "Automatically Verified Data Transfer Protocols," Proc. Fourth ICCC, pp. 749-756,Kyoto, Aug. 1978.
[32] G.J. Holzmann, "PAN: A Protocol Specification Analyzer," Technical Report TM81-11271-5, AT&T Bell Laboratories, Mar. 1981.
[33] G.J. Holzmann, "Tracing Protocols," AT&T Technical J., vol. 64, pp. 2,413-2,434, Dec. 1985.
[34] G.J. Holzmann, "An Improved Protocol Reachability Analysis Technique," Software, Practice and Experience, vol. 18, no. 2, pp. 137-161, 1988.
[35] G.J. Holzmann, "Algorithms for Automated Protocol Verification," AT&T Technical J., vol. 69, no. 1, pp. 32-44, Jan. 1990.
[36] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[37] G.J. Holzmann, "Protocol Design: Redefining The State of the Art," IEEE Software, pp. 17-22, Jan. 1992.
[38] G.J. Holzmann, P. Godefroid, and D. Pirottin, “Coverage Preserving Reduction Strategies for Reachability Analysis,” Proc. 12th Int'l Symp. Protocol Specification, Testing, and Verification, pp. 349-363, 1992.
[39] G.J. Holzmann, "Design and Validation of Protocols: A Tutorial," Computer Networks and ISDN Systems, vol. 25, pp. 981-1,017, 1993.
[40] G.J. Holzmann, "The Theory and Practice of a Formal Method: NewCoRe," Proc. 13th IFIP World Computer Congress, pp. 35-44,Hamburg, Germany, North-Holland, Aug. 1994.
[41] G.J. Holzmann and D. Peled, "An Improvement in Formal Verification," Proc. Seventh FORTE Conf. Formal Description Techniques, pp. 177-194,Bern, Switzerland, Oct. 1994.
[42] G.J. Holzmann, "An Analysis of Bit-State Hashing," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 301-314,Warsaw, Poland, Chapman&Hall, June 1995.
[43] G.J. Holzmann, D. Peled, and M. Yannakakis, "On Nested Depth-First Search," Proc. Second SPINWorkshop, Rutgers Univ., New Brunswick, N.J., DIMACS/32, Am. Math. Soc., Aug. 1996.
[44] G.J. Holzmann, "Designing Bug-Free Protocols with SPIN," The Computer Comm. J., to appear 1997.
[45] G.J. Holzmann, "State Compression in SPIN: Recursive Indexing and Compression Training Runs," Proc. Third SPINWorkshop, Twente Univ., R. Langerak, ed., The Netherlands, Apr. 1997.
[46] H.E. Jensen, K. Larsen, and A. Skou, "Modeling and Analysis of a Collision Avoidance Protocol Using SPINand UPPAAL," Proc. Second SPINWorkshop, Rutgers Univ., New Brunswick, N.J., DIMACS/32, Am. Math. Soc., Aug. 1996.
[47] A. Joesang, "Security Protocol Verification Using SPIN," Proc. First SPINWorkshop, J.-Ch. Gregoire, ed., INRS Quebec, Canada, Oct. 1995.
[48] P. Kars, "The Application of PROMELAand SPINin the BOS Project," Proc. Second SPINWorkshop, Rutgers Univ., New Brunswick, N.J., DIMACS/32, Am. Math. Soc., Aug. 1996.
[49] R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton Univ. Press, 1994.
[50] F.J. Lin, "Two Applications of PROMELA/SPIN," Proc. First SPINWorkshop, J.-Ch. Gregoire, ed., INRS Quebec, Canada, Oct. 1995.
[51] S. Loeffler and A. Serhrouchni, "Protocol Design: From Specification to Implementation," Proc. Fifth Open Workshop for High Speed Networks,Paris, Mar. 1996.
[52] "IEEE Std. 802-2-1985, ISO DIS 8802/2," IEEE Standards for Local Area Networks: Logical Link Control, Published by the IEEE Standards Board, 345 E. 47th Street, New York, NY 10017, USA, 111 pp., ISBN 471-82748-7, 1984. Revised as 802-2-1989 in Aug. 1989.
[53] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[54] E. Najm and F. Olsen, "Reactive EFSMs, Reactive PROMELA/RSPIN," Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS96), pp. 349-368,Passau, Germany, Lecture Notes In Computer Science 1,055, Springer-Verlag, Mar. 1996.
[55] T. Nakatani, "Verification of a Group Address Registration Protocol using PROMELAand SPIN," Proc. Third SPINWorkshop, R. Langerak, ed., Twente Univ., The Netherlands, Apr. 1997.
[56] R.M. Needham and A.J. Herbert, The Cambridge Distributed Computing System.London: Addison-Wesley, 1982.
[57] I. Opris, L. Lewicki, and B.C. Wong, "A Single-Ended Input 12-Bit 20MS/s A/D Converter," IEEE J. Solid-State Circuits, vol. SC-33, no. 12, Dec. 1998, pp. 1898-1903.
[58] D. Peled, "On Projective and Separable Properties," Colloquium on Trees in Algebra and Programming, pp. 291-307,Edinburgh, Scotland, Lecture Notes In Computer Science 787. Springer-Verlag, 1994.
[59] R. Pike, D. Presotto, K. Thompson, and G.J. Holzmann, "Process Sleep and Wakeup on a Shared-Memory Multiprocessor," Proc. the Spring EurOpen Conf., pp. 161-166,Tromso, Norway, 1991.
[60] A. Pnueli, "The Temporal Logic of Programs," Proc. 18th IEEE Symp. Foundations of Computer Science,Providence, R.I., pp. 46-57, 1977.
[61] J.-P. Queille and J. Sifakis, "Specification and Verification of Concurrent Systems in CESAR," Int'l Symp. Programming, pp. 337-351, Lecture Notes in Computer Science 137, Springer-Verlag, Apr. 1982.
[62] B. Rahardjo, "SPINas a Hardware Design Tool," Proc. First SPINWorkshop, J.-Ch. Gregoire, ed., INRS Quebec, Canada, Oct. 1995.
[63] M. Raynal, Distributed Algorithms and Protocol.Chichester: Wiley, 1988.
[64] L.M. Ruane, "Process Synchronization in the UTS Kernel," Computing Systems, Proc. Usenix Conf., vol. 3, no. 3, pp. 387-421, 1990.
[65] T.C. Ruys and R. Langerak, "Validation of Bosch's Mobile Communication Network Architecture with SPIN," Proc. Third SPINWorkshop, R. Langerak, ed., Twente Univ., The Netherlands, Apr. 1997.
[66] T.S. Chan and I. Gorton, "Formal Validation of a High Performance Error Control Protocol Using SPIN," Software, Practice and Experience," vol. 26, no. 1, pp. 105-124, Jan. 1996.
[67] S. Shukla, D.J. Rosenkrantz, and S.S. Ravi, "Simulation and Validation of Self-stabilizing Protocols," Proc. Second SPINWorkshop, Rutgers Univ., New Brunswick, N.J., DIMACS/32, Am. Math. Soc., Aug. 1996.
[68] Proc. First SPINWorkshop, J.-Ch. Gregoire, ed., INRS Quebec, Canada, Oct. 1995. Proc. Second SPINWorkshop, J.-Ch. Gregoire, G.J. Holzmann, and D. Peled, eds., Rutgers Univ., New Brunswick, N.J., DIMACS/32, Am. Math. Soc., Aug. 1996. Proc. Third SPINWorkshop, R. Langerak, ed., Twente Univ., The Netherlands, Apr. 1997.
[69] M. Staskauskas, "Tales from the Front: Industrial Experience with Formal Validation," Proc. First SPINWorkshop, J.-Ch. Gregoire, ed., INRS Quebec, Canada, Oct. 1995.
[70] W.T. Strayer, B.J. Dempsey, and A.C. Weaver, XTP—The Xpress Transfer Protocol.Reading, Mass.: Addison-Wesley, 1992.
[71] A.S. Tanenbaum, Computer Networks, third ed. Prentice Hall, 1996.
[72] R.E. Tarjan, "Depth First Search and Linear Graph Algorithms," SIAM J. Computing, vol. 1, no. 2, pp. 146-160, 1972.
[73] W. Thomas, “Automata on Infinite Objects,” Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, Jan van Leeuwen, ed., Amsterdam 1990.
[74] S. Tripakis and C. Courcoubetis, "Extending PROMELAand SPINfor real-time," Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS96), pp. 329-348,Passau, Germany, Lecture Notes In Computer Science 1,055. Springer-Verlag, Mar. 1996.
[75] P. Tullmann, J. Turner, J. McCorquodale, J. Lepreau, A. Chitturi, and G. Back, "Formal Methods: A Practical Tool for OS Implementers," Proc. HotOS-VI, Sixth IEEE Workshop Hot Topics in Operating Systems,Cape Cod, Mass., May 1997.
[76] R. Nalumasu and G. Gopalakrishnan, "Explicit Enumeration Based on Verification Made Memory Efficient," Proc. Conf. Computer Hardware Description Languages (CHDL'95), pp. 617-622,Chiba, Japan, 1995.
[77] M.Y. Vardi and P. Wolper, "An Automata-Theoretic Approach to Automatic Program Verification," Proc. First IEEE Symp. Logic in Computer Science, pp. 322-331, 1986.
[78] M.Y. Vardi and P. Wolper, "Reasoning About Infinite Computations," Information and Computation, vol. 115, pp. 1-37, 1994, appeared as a conference paper in 1983.
[79] W. Visser, "Memory Efficient Storage in SPIN," Proc. Second SPINWorkshop, Rutgers Univ., New Brunswick, N.J., DIMACS/32, Am. Math. Soc., Aug. 1996.
[80] A.S. Wenban, J.W. O'Leary, and G.M. Brown, "Codesign of Communication Protocols," Computer, vol. 26, no. 12, pp. 46-52, Dec. 1993.
[81] C.H. West, "General Technique for Communications Protocol Validation," IBM J. Research and Development, vol. 22, no. 3, pp. 393-404, 1978.
[82] P. Wolper, "Expressing Interesting Properties of Programs in Propositional Temporal Logic," Proc. 13th ACM Symp. Principles of Programming Languages, pp. 148-193,St. Petersburg, Fla., Jan. 1986.

Index Terms:
Formal methods, program verification, design verification, model checking, distributed systems, concurrency.
Citation:
Gerard J. Holzmann, "The Model Checker SPIN," IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279-295, May 1997, doi:10.1109/32.588521
Usage of this product signifies your acceptance of the Terms of Use.