MECHANICAL VERIFICATION OF A GENERALIZED PROTOCOL FOR BYZANTINE FAULT-TOLERANT CLOCK SYNCHRONIZATION

被引:0
|
作者
SHANKAR, N
机构
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Schneider [Sch87] generalizes a number of protocols for Byzantine fault-tolerant clock synchronization and presents a uniform proof for their correctness. We present a mechanical verification of Schneider's protocol leading to several significant clarifications and revisions. The verification was carried out with the EHDM system [RvHO91] developed at the SRI Computer Science Laboratory. The mechanically checked proofs include the verification that the egocentric mean function used in Lamport and Melliar-Smith's Interactive Convergence Algorithm [LMS85] satisfies the requirements of Schneider's protocol. Our mechanical verification raises a number of issues regarding the verification of fault-tolerant, distributed, real-time protocols that are germane to the design of a special-purpose logic for such problems.
引用
收藏
页码:217 / 236
页数:20
相关论文
共 50 条
  • [1] Verification of a Byzantine-fault-tolerant self-stabilizing protocol for clock synchronization
    Malekpour, Mahyar R.
    [J]. 2008 IEEE AEROSPACE CONFERENCE, VOLS 1-9, 2008, : 1085 - 1097
  • [2] Fault-tolerant clock synchronization in CAN
    Rodrigues, L
    Guimaraes, M
    Rufino, J
    [J]. 19TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1998, : 420 - 429
  • [3] DYNAMIC FAULT-TOLERANT CLOCK SYNCHRONIZATION
    DOLEV, D
    HALPERN, JY
    SIMONS, B
    STRONG, R
    [J]. JOURNAL OF THE ASSOCIATION FOR COMPUTING MACHINERY, 1995, 42 (01): : 143 - 185
  • [4] FAULT-TOLERANT CLOCK SYNCHRONIZATION VALIDATION METHODOLOGY
    BUTLER, RW
    PALUMBO, DL
    JOHNSON, SC
    [J]. JOURNAL OF GUIDANCE CONTROL AND DYNAMICS, 1987, 10 (06) : 513 - 522
  • [5] Sundial: Fault-tolerant Clock Synchronization for Datacenters
    Li, Yuliang
    Kumar, Gautam
    Hariharan, Hema
    Wassel, Hassan
    Hochschild, Peter
    Platt, Dave
    Sabato, Simon
    Yu, Minlan
    Dukkipati, Nandita
    Chandra, Prashant
    Vandat, Amin
    [J]. PROCEEDINGS OF THE 14TH USENIX SYMPOSIUM ON OPERATING SYSTEMS DESIGN AND IMPLEMENTATION (OSDI '20), 2020, : 1171 - 1186
  • [6] FAULT-TOLERANT CLOCK SYNCHRONIZATION IN DISTRIBUTED SYSTEMS
    RAMANATHAN, P
    SHIN, KG
    BUTLER, RW
    [J]. COMPUTER, 1990, 23 (10) : 33 - 42
  • [7] Fault-tolerant Clock Synchronization with High Precision
    Kinali, Attila
    Huemer, Florian
    Lenzen, Christoph
    [J]. 2016 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI (ISVLSI), 2016, : 490 - 495
  • [8] A NEW FAULT-TOLERANT ALGORITHM FOR CLOCK SYNCHRONIZATION
    WELCH, JL
    LYNCH, N
    [J]. INFORMATION AND COMPUTATION, 1988, 77 (01) : 1 - 36
  • [9] A Byzantine-fault tolerant self-stabilizing protocol for distributed clock synchronization systems
    Malekpour, Mahyar R.
    [J]. Stabilization, Safety, and Security of Distributed Systems, Proceedings, 2006, 4280 : 411 - 427
  • [10] A NEW AND IMPROVED ALGORITHM FOR FAULT-TOLERANT CLOCK SYNCHRONIZATION
    PFLUEGL, MJ
    BLOUGH, DM
    [J]. JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 1995, 27 (01) : 1 - 14