TY - GEN
T1 - Modelng the AODV routing protocol in the ω-calculus
AU - Singh, Anu
AU - Ramakrishnan, C. R.
AU - Smolka, Scott A.
PY - 2006
Y1 - 2006
N2 - Mobile ad hoc wireless networks (MANETs) are autonomous collections of mobile nodes that communicate over wireless links. Formal verification of routing protocols for MANETs requires concise yet property-preserving modeling to correctly verify the model and at the same time also avoid running into the problem of state-space explosion. The characteristics of MANETs that pose challenge to the task of modeling are node mobility and broadcast. We have developed a new modeling formalism, called the co-calculus, to naturally and succinctly model MANET protocols. This paper describes the modeling of AODV, a reactive routing protocol for MANETs, in the co-calculus. We aim to subject the model to formal verification in order to prove properties of the AODV routing protocol.
AB - Mobile ad hoc wireless networks (MANETs) are autonomous collections of mobile nodes that communicate over wireless links. Formal verification of routing protocols for MANETs requires concise yet property-preserving modeling to correctly verify the model and at the same time also avoid running into the problem of state-space explosion. The characteristics of MANETs that pose challenge to the task of modeling are node mobility and broadcast. We have developed a new modeling formalism, called the co-calculus, to naturally and succinctly model MANET protocols. This paper describes the modeling of AODV, a reactive routing protocol for MANETs, in the co-calculus. We aim to subject the model to formal verification in order to prove properties of the AODV routing protocol.
UR - https://www.scopus.com/pages/publications/47949083980
U2 - 10.1109/LISAT.2006.4302655
DO - 10.1109/LISAT.2006.4302655
M3 - Conference contribution
AN - SCOPUS:47949083980
SN - 1424403006
SN - 9781424403004
T3 - 2006 IEEE Long Island Systems, Applications and Technology Conference, LISAT
BT - 2006 IEEE Long Island Systems, Applications and Technology Conference, LISAT
T2 - 2006 IEEE Long Island Systems, Applications and Technology Conference, LISAT
Y2 - 5 May 2006 through 5 May 2006
ER -