Access Restriction

Author Bhargavan, Karthikeyan ♦ Obradovic, Davor ♦ Gunter, Carl A.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2002
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword AODV ♦ Formal verification ♦ HOL ♦ RIP ♦ SPIN ♦ Distance vector routing ♦ Interactive theorem proving ♦ Model checking ♦ Network standards ♦ Routing protocols
Abstract 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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2002-07-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 49
Issue Number 4
Page Count 39
Starting Page 538
Ending Page 576

Open content in new tab

   Open content in new tab
Source: ACM Digital Library