Standard algorithms are known for finding the best routes in a network, for some
given notion of route preference. Their operation succeeds when the
preferences satisfy certain criteria, which can be expressed algebraically.
The Internet has provided a wide variety of route-finding problems for which these
criteria can be hard to verify, and the ambitions of network operators and researchers
are more diverse still.
One solution is to provide
a formal means of describing route preferences
in such a way that their correctness criteria can be automatically verified.
This thesis makes the following contributions:
The examples and applications demonstrate the power of the algebraic approach in
permitting analysis of systems that would otherwise be much more
difficult to treat.
- It shows that analysis of
generic route-finding algorithms can be separated from study of
the specific algebraic structures that encode route preferences.
This separation extends to more complex cases than are typically considered
in this context.
- Lexicographic choice is analyzed in detail,
covering deduction rules for correctness criteria as well as its uses.
Design constraints applicable to interdomain routing protocols are derived from
a study of lexicographic choice for hierarchical networks.
- Previous results on algorithmic correctness have been extended in two ways.
An account has been given
of the relationship between two proof strategies for finding the criteria
associated with the existence of a Nash equilibrium.
This leads to a new proof which is both shorter and more general.
- Multipath routing has been incorporated into the algebraic framework.
This allows unified treatment of both single- and multipath algorithms:
they are the same, but instantiated over different algebras.
Another application of the mathematics allows a rigorous treatment of the
handling of erroneous routes.