Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol

1 April 2003

journal article
research article
Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing

Vol. 14 (3) , 328-337
https://doi.org/10.1007/s001650300009

Abstract

: The IEEE 1394 Root Contention Protocol is an industrial leader election algorithm for two processes in which probability, real time and parameters play an important role. This protocol has been analysed in various case studies, using a variety of verification and analysis methods. In this paper, we survey and compare several of these case studies.

Keywords

This publication has 5 references indexed in Scilit:

Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol
Formal Aspects of Computing, 2003
A theory of timed automata
Published by Elsevier ,2002
VLSI Physical Design Automation
Parallel Algorithms, 1999
Partition refinement in real-time model checking
Published by Springer Nature ,1998
Cryptography and Coding
Published by Springer Nature ,1995