Restricted Broadcast Process Theory

11 years 7 months ago
Restricted Broadcast Process Theory
We present a process algebra for modeling and reasoning about Mobile Ad hoc Networks (MANETs) and their protocols. In our algebra we model the essential modeling concepts of ad hoc networks, i.e. local broadcast, connectivity of nodes and connectivity changes. Connectivity and connectivity changes are modeled implicitly in the semantics, which results in a more compact state space. Our connectivity model supports unidirectional links. A key feature of our algebra is eliminating connectivity information from the specification of a network, and transferring its complexity to the semantics. We give a formal operational semantics for our process algebra, and define equivalence relations on protocols and networks. We show how our algebra can be applied to prove correctness of an ad hoc routing protocol.
Fatemeh Ghassemi, Wan Fokkink, Ali Movaghar
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where SEFM
Authors Fatemeh Ghassemi, Wan Fokkink, Ali Movaghar
Comments (0)