Verification of distributed systems with the axiomatic system of MSVL
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516138 | ||
| 003 | CHVBK | ||
| 005 | 20210128100712.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150101xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0303-1 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0303-1 | ||
| 245 | 0 | 0 | |a Verification of distributed systems with the axiomatic system of MSVL |h [Elektronische Daten] |c [Qian Ma, Zhenhua Duan, Nan Zhang, Xiaobing Wang] |
| 520 | 3 | |a 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. | |
| 540 | |a British Computer Society, 2014 | ||
| 690 | 7 | |a Distributed systems |2 nationallicence | |
| 690 | 7 | |a Temporal logic |2 nationallicence | |
| 690 | 7 | |a Temporal logic programming |2 nationallicence | |
| 690 | 7 | |a MSVL |2 nationallicence | |
| 690 | 7 | |a Theorem proving |2 nationallicence | |
| 700 | 1 | |a Ma |D Qian |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | |
| 700 | 1 | |a Duan |D Zhenhua |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | |
| 700 | 1 | |a Zhang |D Nan |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | |
| 700 | 1 | |a Wang |D Xiaobing |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 103-131 |x 0934-5043 |q 27:1<103 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0303-1 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0303-1 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Ma |D Qian |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Duan |D Zhenhua |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Zhang |D Nan |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Wang |D Xiaobing |u Institute of Computing Theory and Technology, Xidian University, No. 2 South Tai Bai Road, P.O. Box 177, 710071, Xi'an, China |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 103-131 |x 0934-5043 |q 27:1<103 |1 2015 |2 27 |o 165 | ||