On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability

详细信息    查看全文

• 作者：Igor Konnov ; Helmut Veith ; Josef Widder ; ^{widder@forsyte.at}
• 关键词：Model checking ; Fault-tolerant distributed algorithms ; Byzantine faults ; Computational models
• 刊名：Information and Computation
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：252
• 期：Complete
• 页码：95-109
• 全文大小：483 K
• 卷排序：252

文摘

Counter abstraction is a powerful tool for parameterized model checking, if the number of local states of the concurrent processes is relatively small. In recent work, we introduced parametric interval counter abstraction that allowed us to verify the safety and liveness of threshold-based fault-tolerant distributed algorithms (FTDA). Due to state space explosion, applying this technique to distributed algorithms with hundreds of local states is challenging for state-of-the-art model checkers. In this paper, we demonstrate that reachability properties of FTDAs can be verified by bounded model checking. To ensure completeness, we need an upper bound on the distance between states. We show that the diameters of accelerated counter systems of FTDAs, and of their counter abstractions, have a quadratic upper bound in the number of local transitions. Our experiments show that the resulting bounds are sufficiently small to use bounded model checking for parameterized verification of reachability properties of several FTDAs, some of which have not been automatically verified before.