Options
A case study in the mechanical verification of fault tolerance
Publikationstyp
Journal Article
Date Issued
2000-10-01
Sprache
English
Author(s)
Mantel, Heiko
Volume
12
Issue
4
Start Page
473
End Page
487
Citation
Journal of Experimental and Theoretical Artificial Intelligence 12 (4): 473-487 (2000-10-01)
Publisher DOI
Scopus ID
Publisher
Taylor & Francis
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.
Subjects
Automated deduction
Fault tolerance
Formal methods
Modular verification
Re-use of proofs and specifications
Reliable broadcast
DDC Class
004: Informatik