Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394

被引：0
|
作者：
Marco Devillers
David Griffioen
Judi Romijn
Frits Vaandrager
机构：
[1] University of Nijmegen,Computing Science Institute
[2] CWI,Computing Science Institute
[3] CWI,undefined
[4] University of Nijmegen,undefined
来源：
Formal Methods in System Design | 2000年 / 16卷
关键词：
IEEE 1394; protocols; tree identify phase; leader election algorithm; formal methods; concurrency theory; I/O automata; theorem provers; PVS;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
The IEEE 1394 high performance serial multimedia bus protocol allows several components to communicate with each other at high speed. In this paper we present a formal model and verification of a leader election algorithm that forms the core of the tree identify phase of the physical layer of the 1394 protocol.
引用
收藏
页码：307 / 320
页数：13
相关论文
共 50 条
  • [1] 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
  • [2] A Timed Verification of the IEEE 1394 Leader Election Protocol
    Judi Romijn
    [J]. Formal Methods in System Design, 2001, 19 : 165 - 194
  • [3] A timed verification of the IEEE 1394 leader election protocol
    Romijn, J
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (02) : 165 - 194
  • [4] Formal verification of a leader election protocol in process algebra
    Fredlund, LA
    Groote, JF
    Korver, H
    [J]. THEORETICAL COMPUTER SCIENCE, 1997, 177 (02) : 459 - 486
  • [5] 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
  • [6] Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM
    Conrado Daws
    Marta Kwiatkowska
    Gethin Norman
    [J]. International Journal on Software Tools for Technology Transfer, 2004, 5 (2-3) : 221 - 236
  • [7] Parametric verification of the IEEE 1394a Root Contention protocol using LPMC
    Toetenel, H
    Spelberg, RL
    Bandini, G
    [J]. SEVENTH INTERNATIONAL CONFERENCE ON REAL-TIME COMPUTING SYSTEMS AND APPLICATIONS, PROCEEDINGS, 2000, : 207 - 214
  • [8] 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
  • [9] 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
  • [10] 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
12345