English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Fault-tolerant distributed algorithms are central for building reliablespatially distributed systems. Unfortunately, the lack of a canonical preciseframework for fault-tolerant algorithms is an obstacle for both verificationand deployment. In this paper, we introduce a new domain-specific framework tocapture the behavior of fault-tolerant distributed algorithms in an adequateand precise way. At the center of our framework is a parameterized system modelwhere control flow automata are used for process specification. To account forthe specific features and properties of fault-tolerant distributed algorithmsfor message-passing systems, our control flow automata are extended to modelthreshold guards as well as the inherent non-determinism stemming fromasynchronous communication, interleavings of steps, and faulty processes.  We demonstrate the adequacy of our framework in a representative case studywhere we formalize a family of well-known fault-tolerant broadcastingalgorithms under a variety of failure assumptions. Our case study is supportedby model checking experiments with safety and liveness specifications for afixed number of processes. In the experiments, we systematically varied theassumptions on both the resilience condition and the failure model. In allcases, our experiments coincided with the theoretical results predicted in thedistributed algorithms literature. This is giving clear evidence for theadequacy of our model.  In a companion paper, we are addressing the new model checking techniquesnecessary for parametric verification of the distributed algorithms captured inour framework.

Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms