caa a22 4500 475797507 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000601xx s 000 0 eng 10.1023/A:1008764923992 doi (NATIONALLICENCE)springer-10.1023/A:1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394 [Elektronische Daten] [Marco Devillers, David Griffioen, Judi Romijn, Frits Vaandrager] 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. We describe the algorithm formally in the I/O automata model of Lynch and Tuttle, and verify that for an arbitrary tree topology exactly one leader is elected. A large part of our verification has been checked mechanically with PVS, a verification system for higher-order logic. Kluwer Academic Publishers, 2000 IEEE 1394 nationallicence protocols nationallicence tree identify phase nationallicence leader election algorithm nationallicence formal methods nationallicence concurrency theory nationallicence I/O automata nationallicence theorem provers nationallicence PVS nationallicence Devillers Marco Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut Griffioen David Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut Romijn Judi Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut Vaandrager Frits Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut Formal Methods in System Design Kluwer Academic Publishers 16/3(2000-06-01), 307-320 0925-9856 16:3<307 2000 16 10703 https://doi.org/10.1023/A:1008764923992 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008764923992 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Devillers Marco Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut NATIONALLICENCE 700 1- Griffioen David Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut NATIONALLICENCE 700 1- Romijn Judi Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut NATIONALLICENCE 700 1- Vaandrager Frits Computing Science Institute, University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/3(2000-06-01), 307-320 0925-9856 16:3<307 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer