| The task of a routing protocol is to discover and maintain paths between distant points in a network. We study the problem of formal correctness analysis of such protocols. Traditionally, routing protocols have been evaluated by testing. While testing provides useful insights about feasibility of the protocol, its interaction with the environment and generally about the average case behavior, it can not provide guarantees which would limit the worst case behavior. Our formal correctness analysis differs from testing in several aspects: (1) It focuses on a protocol standard, rather than a particular implementation. (2) It considers all possible behaviors, rather than just the average case. (3) It is formal, in the sense that we prove mathematical theorems about routing protocols. (4) It can detect errors which are not visible as performance degradation.; We carried out three case studies, each involving a different routing protocol: (1) A well known distance-vector routing protocol RIP. We proved convergence towards optimal routes, together with a sharp real-time bound for convergence time. (2) A recent routing protocol AODV for mobile “ad hoc” networks. We identified flaws that can lead to loop formation, suggested modifications and proved that the modified protocol is loop free. (3) Currently the only widespread inter-domain routing protocol BGP. We first establish a timeless measure for the speed of convergence. We then refine it into a real-time model of the protocol, which we use to prove a general theorem about an upper bound on convergence time. Finally, we show several practical corollaries of the theorem. |
