Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
Formal verification of standards for distance vector routing protocols
Ist Teil von
Journal of the ACM, 2002-07, Vol.49 (4), p.538-576
Ort / Verlag
New York: ACM
Erscheinungsjahr
2002
Link zum Volltext
Quelle
Alma/SFX Local Collection
Beschreibungen/Notizen
We show how to use an interactive theorem prover, HOL, together with a model checker, SPIN, to prove key properties of distance vector routing protocols. We do three case studies: correctness of the RIP standard, a sharp real-time bound on RIP stability, and preservation of loop-freedom in AODV, a distance vector protocol for wireless networks. We develop verification techniques suited to routing protocols generally. These case studies show significant benefits from automated support in reduced verification workload and assistance in finding new insights and gaps for standard specifications.