Verification of mobile ad hoc networks: An algebraic approach

F. Ghassemi, W.J. Fokkink, A. Movaghar

Research output: Contribution to JournalArticleAcademicpeer-review


We introduced Computed Network Process Theory to reason about protocols for mobile ad hoc networks (MANETs). Here we explore the applicability of our framework in two regards: model checking and equational reasoning. The operational semantics of our framework is based on constrained labeled transition systems (CLTSs), in which each transition label is parameterized with the set of topologies for which this transition is enabled. We illustrate how through model checking on CLTSs one can analyze mobility scenarios of MANET protocols. Furthermore, we show how by equational theory one can reason about MANETs consisting of a finite but unbounded set of nodes, in which all nodes deploy the same protocol. Model checking and equational reasoning together provide us with an appropriate framework to prove the correctness of MANETs. We demonstrate the applicability of our framework by a case study on a simple routing protocol. © 2011 Elsevier B.V. All rights reserved.
Original languageEnglish
Pages (from-to)3262-3282
JournalTheoretical Computer Science
Issue number28
Publication statusPublished - 2011


Dive into the research topics of 'Verification of mobile ad hoc networks: An algebraic approach'. Together they form a unique fingerprint.

Cite this