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
fDate :
6/1/2001 12:00:00 AM
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;
Journal_Title :
Software Engineering, IEEE Transactions on
