A NEW ON-LINE DIAGNOSIS PROTOCOL FOR THE SPIDER FAMILY OF BYZANTINE FAULT TOLERANT ARCHITECTURES

摘要

THIS PAPER PRESENTS THE FORMAL VERIFICATION OF A NEW PROTOCOL FOR ONLINE DISTRIBUTED DIAGNOSIS FOR THE SPIDER FAMILY OF ARCHITECTURES. AN INSTANCE OF THE SCALABLE PROCESSOR-INDEPENDENT DESIGN FOR ELECTROMAGNETIC RESILIENCE (SPIDER) ARCHITECTURE CONSISTS OF A COLLECTION OF PROCESSING ELEMENTS COMMUNICATING OVER A RELIABLE OPTICAL BUS (ROBUS). THE ROBUS IS A SPECIALIZED FAULT-TOLERANT DEVICE THAT GUARANTEES INTERACTIVE CONSISTENCY, DISTRIBUTED DIAGNOSIS (GROUP MEMBERSHIP), AND SYNCHRONIZATION IN THE PRESENCE OF A BOUNDED NUMBER OF PHYSICAL FAULTS. FORMAL VERIFICATION OF THE ORIGINAL SPIDER DIAGNOSIS PROTOCOL PROVIDED A DETAILED UNDERSTANDING THAT LED TO THE DISCOVERY OF A SIGNIFICANTLY MORE EFFICIENT PROTOCOL. THE ORIGINAL PROTOCOL WAS ADAPTED FROM THE FORMALLY VERIFIED PROTOCOL USED IN THE MAFT ARCHITECTURE. IT REQUIRED O(N) MESSAGE EXCHANGES PER DEFENDANT TO CORRECTLY DIAGNOSE FAILURES IN A SYSTEM WITH N NODES. THE NEW PROTOCOL ACHIEVES THE SAME DIAGNOSTIC FIDELITY, BUT ONLY REQUIRES O(1) EXCHANGES PER DEFENDANT. THIS PAPER PRESENTS THIS NEW DIAGNOSIS PROTOCOL AND A FORMAL PROOF OF ITS CORRECTNESS USING PVS.