Formally verified Byzantine agreement in presence of link faults
Tóm tắt
This paper shows that deterministic consensus in synchronous distributed systems with link faults is possible, despite the impossibility result of Gray (1978). Instead of using randomization, we overcome this impossibility by moderately restricting the inconsistency that link faults may cause system-wide. Relying upon a novel hybrid fault model that provides different classes of faults for both nodes and links, we provide a formally verified proof that the m+1-round Byzantine agreement algorithm OMH (Lincoln and Rushby (1993)) requires n > 2f/sub l//sup s/ + f/sub l//sup r/ + f/sub l//sup ra/ + 2(f/sub a/ + f/sub s/) + f/sub o/ + f/sub m/ + m nodes for transparently masking at most f/sub l//sup s/ broadcast and f/sub l//sup r/ receive link faults (including at most f/sub l//sup ra/ arbitrary ones) per node in each round, in addition to at most f/sub a/, f/sub s/, f/sub o/, f/sub m/ arbitrary, symmetric, omission, and manifest node faults, provided that m /spl ges/ f/sub a/ + f/sub o/ + 1. Our approach to modeling link faults is justified by a number of theoretical results, which include tight lower bounds for the required number of nodes and an analysis of the assumption coverage in systems where links fail independently with some probability p.
Từ khóa
#Algorithm design and analysis #Formal verification #Fault tolerant systems #Automation #Computer science #Laboratories #Broadcasting #Failure analysis #Distributed algorithms #Field busesTài liệu tham khảo
10.1145/357172.357176
10.1007/3-540-56922-7_24
10.1109/FTCS.1993.627343
lynch, 1996, Distributed Algorithms
meyer, 1987, Consensus with dual failure modes, Digest of Papers International Symposium on Fault-Tolerant Computing, 48
owre, 1996, PVS: Combining specification, proof checking, and model checking, Computer-Aided Verification CAV'96, 411, 10.1007/3-540-61474-5_91
10.1109/TSE.1986.6312888
pinter, 1985, Distributed agreement in the presence of communication and process failures, Proceedings of the 14th IEEE Convention of Electrical & Electronics Engineers in Israel
10.1145/197917.198115
rushby, 2001, Formal verification of hybrid Byzantine agreement under link faults, Technical re-port Computer Science Laboratory SRI Inter-national
biely, 2001, Message-efficient consensus in presence of hybrid node and link faults, Technical Report 183, 1
walter, 2000, The customizable fault/error model for dependable distributed systems, Theoretical Computer Science
basu, 1996, Simulating reliable links with unreliable links in the presence of process crashes, Proc 10th Workshop Distributed Algorithms (WDAG), 105, 10.1007/3-540-61769-8_8
10.1007/BF01843568
10.1145/42282.42283
gray, 1978, Notes on data base operating systems, Operating Systems An Advanced Course, 465
gong, 1995, Byzantine agreement with authentication: Observations and applications in tolerating hybrid and link faults, Proceedings of Dependable Computing for Critical Applications, 139
10.1109/12.888039
hadzilacos, 1993, Fault-tolerant broadcasts and related problems, Distributed Systems, 97
attiya, 1998, Distributed Computing
10.1007/s004460050016
10.1109/DSN.2001.941391
schmid, 2000, Orthogonal accuracy clock synchronization, Chicago Journal of Theoretical Computer Science, 2000, 3
schmid, 2001, Consensus with oral/written mes-sages: Link faults revisited, Technical Report 183, 1
10.1007/PL00008927
10.1109/RELDIS.1988.25784
10.1109/71.667895