Thlis paper reports on the mechanical verification of the IEEE 1394 root
contention protocol. This is an industrial leader election protocol,
in which timing parameters play an essential role.

A manual verification of this protocol using I/O automata has been
published in [SV99].  We improve the communication model from that paper.
Using the Uppaal2k tool, we investigate the timing constraints on the
parameters which are necessary and sufficient for correct protocol
operation:  by analyzing large numbers of protocol instances with
different parameter values, we derive the required timing constraints.

We explore the use of model checking in combination with stepwise
abstraction. That is, we show that the implementation automaton correctly
implements the specification via several intermediate automata, using
Uppaal to prove the trace inclusion in each step.