Model Checking a Modular-Structured Nonblocking Atomic Commitment Protocol for Asynchronous Distributed Systems

Various fault-tolerant agreement protocols for asynchronous distributed systems can be constructed in a modular way which is based on consensus and failure detectors. However it is difficult to design correct fault-tolerant distributed protocols especially for asynchronous systems; so the development of an efficient framework for verifying the protocols is of importance. In this paper, we focus on a modular-structured nonblocking atomic commitment (NBAC) protocol as a case study and propose a method for verifying it with model checking. In this method, we first construct a model for the NBAC protocol in a modular way and next construct temporal logic formulae expressing the termination, justification and obligation properties of the NBAC protocol. Finally, the efficiency of our method is evaluated through the experimental results obtained from using two model checking tools, SPIN and SMV. We expect that our assume-guarantee model checking approach is applicable to other modular-structured fault-tolerant agreement protocols for asynchronous distributed systems.