Verification of Mobile Ad Hoc Networks

Organisation:	Sharif University of Technology, Tehran (IRAN) Vrije Universiteit, Amsterdam (THE NETHERLANDS)
Method:	CNT mCRL2
Tools used:	CADP (Construction and Analysis of Distributed Processes) mCRL2
Domain:	Communication Protocols.
Period:	2011
Size:	n/a
Description:	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.
Conclusions:	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.
Publications:	[Ghassemi-Fokkink-Movaghar-11] 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 the CADP Web site in PDF or PostScript
Contact:	Wan Fokkink VU University Amsterdam Department of Computer Science Section Theoretical Computer Science Room: T443 De Boelelaan 1081a 1081 HV Amsterdam THE NETHERLANDS Tel: +31 20 598 7735 Fax: +31 20 598 7653 Email: w.j.fokkink@vu.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page