TY - BOOK
T1 - A formal analysis of a dynamic distributed spanning tree algorithm
AU - Mooij, A.J.
AU - Wesselink, J.W.
PY - 2003
Y1 - 2003
N2 - Abstract.
We analyze the spanning tree algorithm in the IEEE 1394.1 draft standard, which correctness has not previously been proved. This algorithm is a fully-dynamic distributed graph algorithm, which, in general, is hard to develop. The approach we use is to formally develop an algorithm that is almost equivalent to it: First, based on a formal specification and an abstraction of the network, we systematically construct an algorithm including its correctness proof. Afterwards we implement this algorithm in terms of IEEE 1394 devices under maintenance of its correctness.
AB - Abstract.
We analyze the spanning tree algorithm in the IEEE 1394.1 draft standard, which correctness has not previously been proved. This algorithm is a fully-dynamic distributed graph algorithm, which, in general, is hard to develop. The approach we use is to formally develop an algorithm that is almost equivalent to it: First, based on a formal specification and an abstraction of the network, we systematically construct an algorithm including its correctness proof. Afterwards we implement this algorithm in terms of IEEE 1394 devices under maintenance of its correctness.
M3 - Report
T3 - Computer science reports
BT - A formal analysis of a dynamic distributed spanning tree algorithm
PB - Technische Universiteit Eindhoven
CY - Eindhoven
ER -