A Case Study in the Mechanical Verification of Fault Tolerance

Heiko Mantel, German Research Center for Artificial Intelligence Ltd., Germany; and Felix C. Gärtner, Darmstadt University of Technology, Germany

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.