Synthesis of Fault-Tolerant Distributed Systems

Abstract. A distributed system is fault-tolerant if it continues to perform correctly even when a subset of the processes becomes faulty. Faulttolerance is highly desirable but often difficult to implement. In this paper, we investigate fault-tolerant synthesis, i.e., the problem of determining whether a given temporal specification can be implemented as a fault-tolerant distributed system. As in standard distributed synthesis, we assume that the specification of the correct behaviors is given as a temporal formula over the externally visible variables. Additionally, we introduce the fault-tolerance specification, a CTL∗ formula describing the effects and the duration of faults. If, at some point in time, a process becomes faulty, it becomes part of the external environment and its further behavior is only restricted by the fault-tolerance specification. This allows us to model a large variety of fault types. Our method accounts for the effect of faults on the values communicat...

• Type: Conference
• Year: 2009
• Where: ATVA
• Authors: Rayna Dimitrova, Bernd Finkbeiner
• Keywords: ATVA 2009, Distributed System, Fault-tolerant, Fault-tolerant Synthesis, Hardware