A case study in the mechanical verification of fault tolerance |
| |
| Authors: | Heiko Mantel Felix C. Gartner |
| |
| Affiliation: | 1. German Research Center for Artificial Intelligence ( DFKI ), Stuhlsatzenhausweg 3 D-66123 Saarbrucken , Germany;2. Department of Computer Science , Darmstadt University of Technology , D - 64283 Darmstadt , Germany |
| |
| Abstract: | To date, there is little evidence that modular reasoning about fault-tolerant systems can simplify the verification process in practice. This question is studied using a prominent example from the fault tolerance literature: the problem of reliable broadcast in point-to-point networks subject 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. |
| |
| Keywords: | Automated Deduction Fault Tolerance Formal Methods Modular Verification Reliable Broadcast Re-USE Of Proofs And Specifications |
|
