Analysis of the Suzuki-Kasami algorithm with SAL model checkers
Analysis of the Suzuki-Kasami algorithm with SAL model checkers
复制标题
使用 SAL 模型检查器分析 Suzuki-Kasami 算法
DOI：
10.1109/cit.2005.76
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
K. Futatsugi
中科院分区：
文献类型：
--
作者：
K. Ogata;K. Futatsugi
我们用SAL模型检验器分析了Suzuki-Kasami分布式互斥算法的互斥特性和锁定自由特性。SAL包括五个不同的模型检查器。在案例研究中，我们使用了两个模型检查器SMC(符号模型检查器)和InfBMC(无限有界模型检查器)。SMC已经得出结论，该算法的有限状态模型具有互斥性质，但发现了与锁定自由性质相反的例子。反例导致了一种可能的修改，使算法不会被锁定。我们还利用inBMC证明了该算法的无限状态模型通过k-归纳法具有互斥性。
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.