Various fault-tolerant agreement protocols for asyn- chronous distributed systems can be constructed in a mod- ular way which is based on consensus and failure detec- tors. 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 eval- uated through the experimental results obtained from using two model checking tools, SPIN and SMV. We expect that our assume-guarantee model checking approach is appli- cable to other modular-structured fault-tolerant agreement protocols for asynchronous distributed systems.