A case study in the mechanical verification of fault tolerance
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; RE-USE OF PROOFS AND SPECIFICATIONS; RELIABLE BROADCAST
Document Type: Research Article
Affiliations: 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
Publication date: 01 October 2000
- Editorial Board
- Information for Authors
- Subscribe to this Title
- Ingenta Connect is not responsible for the content or availability of external websites
- Access Key
- Free content
- Partial Free content
- New content
- Open access content
- Partial Open access content
- Subscribed content
- Partial Subscribed content
- Free trial content