Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm
Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm
复制标题
正式建模和验证 Ricart
DOI：
10.1109/apaqs.2001.990041
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
K. Futatsugi
中科院分区：
文献类型：
--
作者：
K. Ogata;K. Futatsugi
创建高质量软件的一个很有前途的方法是对系统进行形式化建模，用形式规范语言描述模型，并在用编程语言实现系统之前，使用自动模型检查器或交互式定理证明器基于形式文档验证系统是否具有某些期望的属性。系统越复杂，例如分布式系统，方法就越重要。我们将该方法应用于Ricart&Agrawala分布式互斥算法(G.Ricart和A.K.Agrawala，1981)。我们将该算法建模为一个统一的计算模型，用CafeOBJ描述了该模型，并借助CafeOBJ系统验证了该算法实际上是基于CafeOBJ文档的互斥的。
One of the promising approaches to creating quality software is to formally model systems, describe the models in a formal specification language, and verify that the systems have some desirable properties based on the formal documents with an automatic model checker or an interactive theorem prover before the systems are implemented in a programming language. The more complicated the systems are, such as distributed systems, the more important the approach is. We have applied the approach to the Ricart&Agrawala distributed mutual exclusion algorithm (G. Ricart and A. K. Agrawala, 1981). We have modeled the algorithm as a UNITY computational model, described the model in CafeOBJ, and verified that the algorithm is actually mutually exclusive based on the CafeOBJ document with the help of the CafeOBJ system.