Model Checking a Modular-Structured Nonblocking Atomic Commitment Protocol for Asynchronous Distributed Systems
Eun-Hye Choi, Keishi Okamoto, Tatsuhiro Tsuchiya, Tohru Kikuno · 2009
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.