Sharif University of Technology, Tehran (IRAN)
Vrije Universiteit, Amsterdam (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
Mobile ad hoc networks (MANETs) consist of mobile nodes equipped
with wireless transceivers to communicate with each other directly or
along multihop paths. Two nodes can effectively communicate if they are
located in the communication range of each other, defined by the
underlying topology. Wireless communication is inherently unreliable
(due to noise in the environment) and mobility of nodes makes the
underlying topology dynamic. These characteristics require a suitable
framework for the modeling and verification of MANETs.
Restricted Broadcast Process Theory (RBPT) enables to specify and verify MANET protocols, taking into account mobility of nodes. Topology changes are modeled implicitly in the semantics, and thus one can verify a network with respect to arbitrary topology changes. Computed Network Process Theory (CNT) is an extension of RBPT with so-called computed network terms and auxiliary operators. The operational semantics of CNT is given by constrained labeled transition systems (CLTSs), in which each transition label is parameterized by a set of topologies for which this transition is enabled. This work enhances and illustrates the applicability of CNT for the analysis of MANETs using model checking and equational reasoning.
The approach is illustrated on a simple routing protocol similar to ad hoc on-demand distance vector (AODV) routing protocol. The CNT specification is converted into a CLTS using the mCRL2 toolset. The existence of routing loops in the presence of link breakages was checked using the EVALUATOR model checker of CADP, and enabled to revise the protocol and make sure that it correctly routes data from a source to a destination for the scenarios leading to one link breakage with three middle nodes. Then, the correctness of the revised protocol for an arbitrary number of link breakages and number of middle nodes is shown using a symbolic verification technique based on cones and foci points.
Algebraic techniques combined with model checking enable to examine
the behavior of a MANET for arbitrary mobility of nodes through one
model, without the need to specify mobility changes. The proposed
framework is applicable in wireless networks in which communication
is based on non-blocking and lossy local broadcast, if it is extended
with a static location binding operator that restricts the arbitrary
mobility of nodes.
Fatemeh Ghassemi, Wan Fokkink, and Ali Movaghar.
"Verification of Mobile Ad Hoc Networks: An Algebraic Approach".
Theoretical Computer Science 412(28):3262-3282, 2011.
Available on-line from: http://www.cs.vu.nl/~wanf/pubs/algebraic-manet.pdf
or from our FTP site in PDF or PostScript
VU University Amsterdam
Department of Computer Science
Section Theoretical Computer Science
De Boelelaan 1081a
1081 HV Amsterdam
Tel: +31 20 598 7735
Fax: +31 20 598 7653
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|