Sciweavers

JACM
2002

Formal verification of standards for distance vector routing protocols

13 years 3 months ago
Formal verification of standards for distance vector routing protocols
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. Categories and Subject Descriptors: C.2.2 [Computer-Communication Networks]: Network Protocols--protocol verification, routing protocols; C.2.6 [Computer-Communication Networks]: Internet working--routers, standards; D.2.4 [Software Engineering]: Software/Program Verification--correctness proofs; formal methods, model checking; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and R...
Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gu
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 2002
Where JACM
Authors Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter
Comments (0)