This Article
	Subscribers, please Login Purchase article: $19 PDF HTML IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Gerard J. Holzmann

The Model Checker SPIN

May 1997 (vol. 23 no. 5)

pp. 279-295

[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.