Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm
Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm
复制标题
铃木的形式分析
DOI：
10.1007/978-0-387-35496-5_13
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
K. Futatsugi
中科院分区：
文献类型：
--
作者：
K. Ogata;K. Futatsugi
由于并行和分布式算法容易受到微妙错误的影响，而这些错误在通常的操作中不太可能被检测到，因此仅进行测试不足以减少错误。因此，有必要对这些算法进行形式化分析，以确认它们具有所需的性质。本文描述了对Suzuki&Kasami分布式互斥算法进行形式化分析的案例。在实例研究中，该算法使用了一种称为观测转移系统(OTS‘s)的类单位模型来建模，该模型已在CafeOBJ中进行了描述，并在CafeOBJ系统的帮助下验证了该算法是互斥和无锁定的。在算法无锁定的验证中，我们发现了验证所必需的隐藏假设，这在Suzuki和Kasami的原始论文中没有明确提到。
Since parallel and distributed algorithms are subject to subtle errors that are unlikely to be detected in usual operation, only testing is not enough to reduce errors. Thus, it is necessary to formally analyze such algorithms in order to confirm that they have desirable properties. This paper describes the case study that Suzuki&Kasami distributed mutual exclusion algorithm is formally analyzed. In the case study, the algorithm has been modeled using UNITY-like models called observational transition systems (OTS'S), the model has been described in CafeOBJ, and it has been verified that the algorithm is mutually exclusive and lockout free with the help of CafeOBJ system. In the verification that the algorithm is lockout free, we have found a hidden assumption necessary for the verification, which is not explicitly mentioned in the original paper written by Suzuki and Kasami.