| Model Checking a Modular-Structured Nonblocking Atomic Commitment Protocol for Asynchronous Distributed Systems (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Various principal fault-tolerant agreement protocols for asynchronous distributed systems, such as atomic commitment and view synchrony, can be constructed in a modular way which is based on consensus and failure detectors. Since, however, it is difficult to design correct fault-tolerant distributed protocols especially for asynchronous systems, the development of an efficient framework for verifying the fault-tolerant distributed agreement protocols is of importance. In this paper, we focus on a modularstructured nonblocking atomic commitment (NBAC) protocol as a case study and propose a method to verify the protocol by model checking. In the proposed method, we first construct a model for the NBAC protocol in a modular way by composing a behavior model for unreliable failure detector and a behavior model for distributed computing nodes participating in the target protocol. We next construct temporal logic formulae expressing the termination, justification, and obligation properties of the NBAC protocol assuming that the properties that the consensus module and the unreliable failure detectors should provide are guaranteed. Finally, the efficiency of our method is evaluated through the experimental results obtained from using two model checking tools, SPIN and SMV. We conjecture that our assume-guarantee model checking approach given in this paper is applicable to generic modular-structured fault-tolerant agreement protocols for asynchronous distributed systems. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||