×

zbMATH — the first resource for mathematics

Verification of distributed systems with the axiomatic system of MSVL. (English) Zbl 1328.68032
Summary: 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.

MSC:
68M14 Distributed systems
68N17 Logic programming
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
METATEM; mCRL2
PDF BibTeX Cite
Full Text: DOI
References:
[1] Armbrust, M; Fox, A; Griffith, R; Joseph, AD; Katz, R; Konwinski, A; Lee, G; Patterson, D; Rabkin, A; Stoica, I; Zaharia, M, A view of cloud computing, Commun ACM, 53, 50-58, (2010)
[2] Barringer H, Fisher M, Gabbay D, Gough G, Owens R (1990) METATEM: a framework for programming in temporal logic. In: Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, REX workshop. Springer-Verlag New York, Inc., New York, pp 94-129
[3] Bledsoe W, Loveland D (1984) Automating theorem proving: after 25 years. American Mathematical Society, Providence · Zbl 0545.00023
[4] Bruns G (1996) Distributed systems analysis with CCS. Prentice Hall PTR, Englewood Cliffs
[5] Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching timed temporal logic. In: LNCS, vol 131. Springer, Bertin, pp 52-71
[6] Cranen S, Groote J, Keiren JJA, Stappers FPM, Vink EP, Wesselink W, Willemse TA (2013) An overview of the mCRL2 toolset and its recent advances. In: Piterman N, Smolka SA (eds) Tools and algorithms for the construction and analysis of systems, vol 7795. Lecture notes in computer science, Springer, Berlin, pp 199-213 · Zbl 1381.68198
[7] Clarke, EM, Grumberg O, Peled D (2008) Model checking. The MIT Press, Cambridge
[8] Chen, B-S; Yeh, T, Formal specification and verification of distributed systems, Trans Soft Eng SE-, 9, 710-722, (1983) · Zbl 0519.68035
[9] Déharbe, D, Integration of SMT-solvers in B and event-B development environment, Sci Comput Progr, 78, 310-326, (2013) · Zbl 1264.68056
[10] Duan Z, Koutny M, Holt C (1994) Projection in temporal logic programming. In: Proceedings of logic programming and automated reasoning. LNAI, vol 822, pp 333-344
[11] Dong J, Sun J, Liu Y (2013) Build your own model checker in one month. In: Poceedings of ICSE13, pp 1481-1483
[12] Duan Z, Tian C (2008) A unified model checking approach with projection temporal logic. In: Proceedings of ICFEM08, pp 167-186 · Zbl 1264.68056
[13] Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis, University of Newcastle Upon Tyne, May 1996
[14] Duan Z (2006) Temporal logic and temporal logic programming language. Science Press, Beijing
[15] Fisher M (1994) A survey of concurrent metatem: the language and its applications. In: Temporal logic. Lecture notes in computer science, vol 827. Springer, Berlin, pp 480-505 · Zbl 0949.68532
[16] Hennessy M (2007) A distributed Pi-calculus. Cambridge University Press, Cambridge · Zbl 1125.68082
[17] Hoare, CAR, Communicating sequential processes, Commun ACM, 21, 666-677, (1978) · Zbl 0383.68028
[18] Jensen K (1991) Coloured petri nets: a high level language for system design and analysis. In: Rozenberg G (ed) Advances in petri nets 1990, vol 483. Lecture notes in computer science, Springer, Berlin, pp 342-416
[19] Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University · Zbl 0383.68028
[20] Lamport, L, The temporal logic of actions, ACM Trans Program Lang Syst, 16, 872-923, (1994)
[21] Lynch NA, Tuttle MR (1987) Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the sixth annual ACM symposium on principles of distributed computing. PODC ’87, pp 137-151 · Zbl 0357.68067
[22] Milner R (1982) A calculus of communicating systems. Springer-Verlag New York, Inc., Secaucus · Zbl 0452.68027
[23] Milner R (1999) Communicating and mobile systems: the π-calculus. Cambridge University Press, Cambridge · Zbl 0942.68002
[24] Moszkowski BC (1986) Executing temporal logic programs. PhD thesis, Cambridge Uniersity, Cambridge · Zbl 0565.68003
[25] Manna Z, Pnueli A (1992) Temporal logic of reactive and concurrent systems. Springer, Berlin · Zbl 0753.68003
[26] Mo D, Wang X, Duan Z (2011) Asynchronous communication in MSVL. In: Proceeding of ICFEM2011. LNCS, vol 6991, pp 82-97
[27] Peterson, JL, Petri nets, ACM Comput Surv, 9, 223-252, (1977) · Zbl 0357.68067
[28] Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th annal IEEE symposium on foudations of computer science. IEEE Computer Society, pp 46-57 · Zbl 0383.68028
[29] Ricart, G; Agrawala, AK, An optimal algorithm for mutual exclusion in computer networks, Commun ACM, 24, 9-17, (1981)
[30] Rodriguez-Navas, G; Proenza, J, Using timed automata for modeling distributed systems with clocks: challenges and solutions, IEEE Trans Softw Eng, 39, 857-868, (2013)
[31] Tang CS (1983) Toward a unified logic basis for programming languages. In: Proceedings of IFIP congress. Elsevier Science, North Holland, pp 425-429
[32] Tian C, Duan Z (2011) Expressiveness of propositional projection temporal logic with star. Theor Comput Sci 412:1729-1744 · Zbl 1221.03018
[33] Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J (2009) Formal methods: practice and experience. Comput Surv 41(4):19: 1-19:36
[34] Yang, X; Duan, Z; Ma, Q, Axiomatic semantics of projection temporal logic programs, Math Struct Comput Sci, 20, 865-914, (2010) · Zbl 1213.68186
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.