This Article 
 Bibliographic References 
 Add to: 
Comments on 'The Model Checker SPIN'
June 2001 (vol. 27 no. 6)
pp. 573-576

Abstract—We report an error in a verification model in [4] and present a revised model with verification result. Our result explains the reason why SPIN found the race condition in the synchronization algorithm. We also show that the suggested fix in [4] is incorrect.

[1] P. Brémond-Gregoire, J.Y. Choi, and I. Lee, “A Complete Axiomatization of Finite-State ACSR Processes,” Information and Computation, no.138, 1997.
[2] D. Clarke, I. Lee, and H.-R. Xie, “VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems,” J. Computer Software Eng., vol. 3, no. 2, 1995.
[3] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[4] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[5] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
[6] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[7] L.M. Ruane, “Process Synchronization in the UTS Kernel,” Computing Systems, vol. 3, no. 3, pp. 387-421, 1990.

Index Terms:
SPIN, ACSR, LTL, model checking, process scheduling.
Ki-Seok Bang, Jin-Young Choi, Chuck Yoo, "Comments on 'The Model Checker SPIN'," IEEE Transactions on Software Engineering, vol. 27, no. 6, pp. 573-576, June 2001, doi:10.1109/32.926177
Usage of this product signifies your acceptance of the Terms of Use.