Published Articles >> Table of Contents >> Abstract

2004 International Conference on Dependable Systems and Networks (DSN'04)   p. 485
Analyses of the Reverse Path Forwarding Routing Algorithm
Christie Bolton, Oxford University Computing Laboratory
Gavin Lowe, Oxford University Computing Laboratory

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DSN.2004.1311918
Send link to a friend

Abstract
The reverse path forwarding algorithm is a protocol for distributing messages throughout networks. The intention is to preserve correctness-messages sent will eventually be received by all nodes in the originator's connected component-whilst minimising the number of propagations of each message. We use a variety of analysis techniques to identify necessary additional constraints, and to prove correctness under these conditions. In particular we present counter examples found by the model-checkers FDR and the Alloy Analyzer, illustrating that the protocol is incorrect if the cost of links is dependent upon the node using that link. We then consider the case where the cost of links is independent of the node using that link; we use a special-purpose network sampling program to increase confidence in the correctness of this stricter protocol, and then perform a hand-proof to verify correctness. We conclude with a discussion of the suitability of these techniques for reasoning about protocols of this complexity.
Back to Top Additional Information
Citation:  Christie Bolton, Gavin Lowe, "Analyses of the Reverse Path Forwarding Routing Algorithm," dsn, p. 485,  2004 International Conference on Dependable Systems and Networks (DSN'04),  2004