A Unified Fault-Tolerance Protocol

• ABSTRACT:
  
  Davies and Wakerly show that Byzantine fault tolerance can be achieved by a cascade of broadcasts and middle value select functions.  We present an extension of the Davies and Wakerly protocol, the unified protocol, and its proof of correctness.  The unified protocol provides fault-tolerance as a service to other protocols.  We prove that it satisfies validity and agreement properties for communication of exact values.  We then introduce bounded communication error into the model. Inexact communication is inherent for clock synchronization protocols.  We prove that validity and agreement properties hold for inexact communication, and that exact communication is a special case.  As a running example, we illustrate the unified protocol using the SPIDER family of fault-tolerant architectures.  In particular we demonstrate that the SPIDER interactive consistency, distributed diagnosis, and clock synchronization protocols are instances of the unified protocol.

• BIBTEX:
  

  @InProceedings{unified,
    author =    {Paul Miner and Alfons Geser and Lee Pike and Jeffery Maddalon},
    title =     {A Unified Fault-Tolerance Protocol},
    year =      {2004},
    pages =     {167--182},
    booktitle = {Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems ({FORMATS-FTRTFT})},
    editor =    {Yassine Lakhnech and Sergio Yovine},
    volume =    {3253},
    series =    {Lecture Notes in Computer Science},
    publisher = {Springer},
    note =      {Available at \url{https://leepike.github.io/pub_pages/unified.html}}}

• PAPER DOWNLOAD: pdf

• PVS FILES DOWNLOAD: PVS dump file