Analysis of the Suzuki-Kasami algorithm with the Maude model checker
Analysis of the Suzuki-Kasami algorithm with the Maude model checker
复制标题
使用 Maude 模型检查器分析 Suzuki-Kasami 算法
DOI：
10.1109/apsec.2005.40
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
K. Futatsugi
中科院分区：
文献类型：
--
作者：
K. Ogata;K. Futatsugi
我们报告了一个案例研究，其中使用 Maude 模型检查器来分析 Suzuki-Kasami 分布式互斥算法的互斥性和锁定自由性。 Maude 是一种基于隶属方程逻辑和重写逻辑的规范和编程语言/系统，配备了模型检查设施。 Maude 允许用户在要进行模型检查的规范中使用抽象数据类型，包括归纳定义的数据类型，这是 Maude 模型检查器的优点之一。因此，案例研究中使用的队列不必以更基本的数据类型进行编码。在案例研究中，莫德模型检查器发现了算法是免锁定的反例，这导致了一种可能的修改，使算法免锁定。
We report on a case study in which the Maude model checker has been used to analyze the Suzuki-Kasami distributed mutual exclusion algorithm with respect to the mutual exclusion property and the lockout freedom property. Maude is a specification and programming language/system based on membership equational logic and rewriting logic, equipped with model checking facilities. Maude allows users to use abstract data types, including inductively defined ones, in specifications to be model checked, which is one of the advantages of the Maude model checker. Hence, queues, which are used in the case study, do not have to be encoded in more basic data types. In the case study, the Maude model checker has found a counterexample that the algorithm is lockout free, which has led to one possible modification that makes the algorithm lockout free.