Felix C. Gärtner: Specifications for fault tolerance: A comedy of failures. Technical Report TUD-BS-1998-03, Department of Computer Science, Darmstadt University of Technology, Darmstadt, Germany, October 1998.


Abstract

A substantial difficulty in rigorously reasoning about fault tolerant distributed algorithms is the necessity to formally describe faulty behavior. In this paper, we present a unified and formal approach to specify such behavior. It is based on the observation that faulty behavior can be regarded as a special form of (programmable) system behavior. Consequently, a failure model is defined to be a program transformation which can be used to evaluate the correctness properties of fault tolerant algorithms. We re-formulate several failure models which are pervasive in the literature in terms of our approach and show some interesting relations between them. In order to show the feasibility of this approach, we apply our methodology to the problem of reliable broadcast.
Available as gnuzipped Postscript file.


Felix Gärtner (felix@informatik.tu-darmstadt.de)