Automatic Verification of Fault-Tolerant Register Emulations

详细信息    查看全文

• 作者：Paul C. Attie ; Hana Chockler
• 关键词：Distributed algorithms ; parametrized systems ; fault-tolerance ; crash failures ; register emulation ; automatic verification ; model checking
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2006
• 出版时间：3 February 2006
• 年：2006
• 卷：149
• 期：1
• 页码：49-60
• 全文大小：232 K

文摘

The design and verification of fault-tolerant distributed algorithms is a complicated task. Usually, the proof of correctness is done manually, and thus depends on the skill of the prover. Using automated verification methods, such as model checking, can greatly simplify the verification. However, model checking of distributed algorithms is often intractable because of the state-explosion problem. In this paper we present a novel approach to verification of quorum-based distributed register emulation algorithms with undetectable crash failures of processes. Our approach is based on projection and abstraction and allows us to reduce the task of model-checking the whole system to fair model-checking of subsystems consisting of a constant number of processes. Our method is highly scalable and can be applied to a large class of algorithms. Aside from efficient verification, it can also be used for finding redundancies in existing algorithms.