Issue No.06 - June (2001 vol.27)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.926177
<p><b>Abstract</b>—We report an error in a verification model in [<ref rid="bibE05734" type="bib">4</ref>] 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 [<ref rid="bibE05734" type="bib">4</ref>] is incorrect.</p>
SPIN, ACSR, LTL, model checking, process scheduling.
Jin-Young Choi, Ki-Seok Bang, "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