Fifth International Conference on Computer and Information Technology (CIT'05) Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers Shanghai, China September 21-September 23 ISBN: 0-7695-2432-X
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CIT.2005.76
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 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.
Citation:
Kazuhiro Ogata, Kokichi Futatsugi, "Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers," cit, pp.937-943, Fifth International Conference on Computer and Information Technology (CIT'05), 2005 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb