Construction and verification of routing algebras

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 operations 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. - 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. 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.EThOS - Electronic Theses Online ServiceGBUnited Kingdo