Felix C. Gärtner: An exercise in systematically deriving fault-tolerance specifications. Technical Report TUD-BS-1999-01, Department of Computer Science, Darmstadt University of Technology, Darmstadt, Germany, March 1999.

Abstract

To rigorously prove that a system is correct under normal system operation requires a formal correctness specification. In the context of fault tolerance, correctness means that a system must be correct even if some specified faults occur. The correctness conditions in the former and in the latter case are however not necessarily the same. This is because correctness specifications for fault tolerance must often take the behavior of faulty components into account. In this paper we perform a case study on the interrelations between problem specifications in ideal environments and in faulty ones. The problem considered is that of consensus and the failure model used is crash. The goal of this research is to uncover the influences that specific failure models have on problem specifications so that fault-tolerance specifications can be systematically derived. As this is work in progress, the ideas herein are partly half-baked and deserve some additional discussion.

Available as gnuzipped Postscript file.

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