학술논문
Analysis of the Suzuki-Kasami algorithm with SAL model checkers
Document Type
Conference
Author
Source
The Fifth International Conference on Computer and Information Technology (CIT'05) Computer and Information Technology Computer and Information Technology, 2005. CIT 2005. The Fifth International Conference on. :937-943 2005
Subject
Language
Abstract
We report on a case study in which SAL model checkers have been used to analyze the Suzuki-Kasami distributed mutual exclusion algorithm with respect to the mutual exclusion property and the lockout freedom property. SAL includes five different model checkers. In the case study, we have used two model checkers SMC (symbolic model checker) and infBMC (infinite bounded model checker). SMC has concluded that a finite-state model of the algorithm has the mutual exclusion property, but has found a counterexample to the lockout freedom property. The counterexample has led to one possible modification that makes the algorithm lockout free. We have also used infBMC to prove that an infinite-state model of the algorithm has the mutual exclusion property by k-induction.