DocumentCode
1497591
Title
Comments on "The Model Checker SPIN"
Author
Bang, Ki-Seok ; Choi, Jin-Young ; Yoo, Chuck
Author_Institution
Dept. of Comput. Sci. & Eng., Korea Univ., Seoul, South Korea
Volume
27
Issue
6
fYear
2001
fDate
6/1/2001 12:00:00 AM
Firstpage
573
Lastpage
576
Abstract
The paper by G.J. Holzmann (see ibid., vol.23, no.5, p.279-95, 1997) describes how to apply SPIN to the verification of a synchronization algorithm (L.M. Ruane, 1990) in process scheduling of an operating system. We report an error in the verification model presented by G.J. Holzmann 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 by G.J. Holzmann is incorrect.
Keywords
hazards and race conditions; operating systems (computers); program verification; scheduling; synchronisation; ACSR; LTL; Model Checker; SPIN; operating system; process scheduling; race condition; synchronization algorithm; verification model; verification result; Availability; Computer science; Operating systems; Scheduling algorithm; Software algorithms;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/32.926177
Filename
926177
Link To Document