A Case Study in the Mechanical Verification of Fault Tolerance

May 2000

Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2000)

Volume

Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2000)

All Papers

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.