Verification of distributed systems with the axiomatic system of MSVL
Verification of distributed systems with the axiomatic system of MSVL
复制标题
DOI：
10.1007/s00165-014-0303-1
复制
发表时间：
2014-07
影响因子：
1
通讯作者：
Q. Ma;Zhenhua Duan;N. Zhang;Xiaobing Wang
中科院分区：
文献类型：
--
作者：
Q. Ma;Zhenhua Duan;N. Zhang;Xiaobing Wang
由于分布式系统本质上是并发和异步的，因此验证分布式系统对我们来说是一个挑战。MSVL是一种有用的时间逻辑程序设计语言，并建立了它的公理体系。然而，MSVL的公理系统缺乏管理异步通信的机制，这使得它无法处理分布式系统。因此，为了用演绎的方式验证具有MSVL的分布式系统，本文的动机是用新的异步通信公理扩展MSVL的公理系统。为此，我们首先形式化了异步通信命令的状态公理，然后证明了状态公理的正确性和完备性。进一步，为了证明MSVL的扩展公理系统如何适用于分布式系统，我们将其应用于著名的Ricart-Agrawala （RA）算法，该算法是一种具有无限状态空间的分布式互斥算法。为此，我们使用MSVL对RA算法建模，指定所需的属性，然后根据先到先服务的属性验证RA算法的实例。
Since distributed systems are inherently concurrent and asynchronous, it is a challenge for us to verify distributed systems. MSVL is a useful temporal logic programming language and its axiomatic system has been established. However, the axiomatic system of MSVL lacks mechanisms to manage asynchronous communication, which makes it cannot deal with distributed systems. Thus, to verify distributed systems with MSVL in a deductive way, this paper is motivated to extend the axiomatic system of MSVL with new axioms for asynchronous communication. To this end, firstly we formalize state axioms regarding asynchronous communication commands and then prove the soundness and completeness. Further, to demonstrate how the extended axiomatic system of MSVL works for distributed systems, we apply it to the well-known Ricart–Agrawala (RA) algorithm, which is a distributed mutual exclusion algorithm and has an infinite state space. To do this, we model the RA algorithm with MSVL, specify the desired properties and then verify an instance of the RA algorithm with respect to the first-come-first-served property.