Sciweavers

Share
IEEECIT
2005
IEEE

Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers

10 years 7 months ago
Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers
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   -induction.
Kazuhiro Ogata, Kokichi Futatsugi
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where IEEECIT
Authors Kazuhiro Ogata, Kokichi Futatsugi
Comments (0)
books