Distributed algorithms are hard to develop, to understand, and to analyze. This is especially so for algorithms for dynamically changing network structures.
this thesis carries out a formal analysis on one such algorithm. It is formally modelled using I/O automata, and some crucial properties are formally established. Additionally, the algorithm is implemented in Java 1.5, making use if Java’s new concurrent utilities package.
| supervisors | Martin Steffen |