Heiko Mantel and Felix C. Gärtner:
A case study in the mechanical verification of fault tolerance.
Technical Report TUD-BS-1999-08, Department of
Computer Science, Darmstadt University of Technology,
Darmstadt, Germany, November 1999.
Abstract
To date, there is little evidence that modular reasoning about
fault-tolerant systems can simplify the verification process
in practice. We study this question using a prominent example from
the fault tolerance literature: the problem of reliable broadcast in
point-to-point networks opposed to crash failures of processes. The
experiences from this case study show how modular specification
techniques and rigorous proof re-use can indeed help in such
undertakings.
Available as gnuzipped Postscript file.
Felix Gärtner (felix@informatik.tu-darmstadt.de)