Formal verification of a leader election protocol in process algebra

被引：15
|
作者：
Fredlund, LA
Groote, JF
Korver, H
机构：
[1] CTR WISKUNDE & INFORMAT,NL-1098 SJ AMSTERDAM,NETHERLANDS
[2] SWEDISH INST COMP SCI,S-16428 KISTA,SWEDEN
来源：
THEORETICAL COMPUTER SCIENCE | 1997年 / 177卷 / 02期
基金：
瑞典研究理事会;
关键词：
D O I：
10.1016/S0304-3975(96)00256-3
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In 1982 Dolev, et al. [10] presented an O(nlogn) unidirectional distributed algorithm for the circular extrema-finding (or leader-election) problem. At the same time Peterson came up with a nearly identical solution. In this paper, we bring the correctness of this algorithm to a completely formal level. This relatively small protocol, which can be described on half a page, requires a rather involved proof for guaranteeing that it behaves well in all possible circumstances. To our knowledge, this is one of the more advanced case-studies in formal verification based on process algebra.
引用
收藏
页码：459 / 486
页数：28
相关论文
共 50 条
  • [1] Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394
    Marco Devillers
    David Griffioen
    Judi Romijn
    Frits Vaandrager
    [J]. Formal Methods in System Design, 2000, 16 : 307 - 320
  • [2] Verification of a leader election protocol: Formal methods applied to IEEE 1394
    Devillers, M
    Griffioen, D
    Romijn, J
    Vaandrager, F
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2000, 16 (03) : 307 - 320
  • [3] Formal Verification of Ring-based Leader Election Protocol using Predicate Diagrams
    Nugraheni, Cecilia E.
    [J]. INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2009, 9 (08): : 1 - 8
  • [4] A Timed Verification of the IEEE 1394 Leader Election Protocol
    Judi Romijn
    [J]. Formal Methods in System Design, 2001, 19 : 165 - 194
  • [5] A timed verification of the IEEE 1394 leader election protocol
    Romijn, J
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (02) : 165 - 194
  • [6] Probabilistic verification of hierarchical leader election protocol in dynamic systems
    Yu Zhou
    Nvqi Zhou
    Tingting Han
    Jiayi Gu
    Weigang Wu
    [J]. Frontiers of Computer Science, 2018, 12 : 763 - 776
  • [7] Verification of HS Leader Election Protocol using a Mechanized Framework
    Samanta, Tapas
    Sarkar, Dipankar
    [J]. 2012 NATIONAL CONFERENCE ON COMPUTING AND COMMUNICATION SYSTEMS (NCCCS), 2012, : 304 - 308
  • [8] Probabilistic verification of hierarchical leader election protocol in dynamic systems
    Zhou, Yu
    Zhou, Nvqi
    Han, Tingting
    Gu, Jiayi
    Wu, Weigang
    [J]. FRONTIERS OF COMPUTER SCIENCE, 2018, 12 (04) : 763 - 776
  • [9] VERIFICATION OF AN ALTERNATING BIT PROTOCOL BY MEANS OF PROCESS ALGEBRA
    BERGSTRA, JA
    KLOP, JW
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1986, 215 : 9 - 23
  • [10] Semi-formal development of a fault-tolerant leader election protocol in Erlang
    Arts, T
    Claessen, K
    Svensson, H
    [J]. FORMAL APPROACHES TO SOFTWARE TESTING, 2005, 3395 : 140 - 154
12345