2012/10/14 by Annu John, John, Annu, Igor Konnov +7
Computer Science · Engineering · #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Parallel #Parallel Computing and Optimization Techniques #Radiation Effects in Electronics #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.1210.3839
openalex publication_date 2012/10/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Fault-tolerant distributed algorithms are central for building reliable\nspatially distributed systems. Unfortunately, the lack of a canonical precise\nframework for fault-tolerant algorithms is an obstacle for both verification\nand deployment. In this paper, we introduce a new domain-specific framework to\ncapture the behavior of fault-tolerant distributed algorithms in an adequate\nand precise way. At the center of our framework is a parameterized system model\nwhere control flow automata are used for process specification. To account for\nthe specific features and properties of fault-tolerant distributed algorithms\nfor message-passing systems, our control flow automata are extended to model\nthreshold guards as well as the inherent non-determinism stemming from\nasynchronous communication, interleavings of steps, and faulty processes.\n We demonstrate the adequacy of our framework in a representative case study\nwhere we formalize a family of well-known fault-tolerant broadcasting\nalgorithms under a variety of failure assumptions. Our case study is supported\nby model checking experiments with safety and liveness specifications for a\nfixed number of processes. In the experiments, we systematically varied the\nassumptions on both the resilience condition and the failure model. In all\ncases, our experiments coincided with the theoretical results predicted in the\ndistributed algorithms literature. This is giving clear evidence for the\nadequacy of our model.\n In a companion paper, we are addressing the new model checking techniques\nnecessary for parametric verification of the distributed algorithms captured in\nour framework.\n