Modeling Routing Protocols in Adhoc Networks

Regarding increasing popularity of Ad hoc networks, the routing protocols employed in these networks should be validated before deployment. Formal methods are used nowadays to find defects in protocols specification. In this paper. we explain different methods of formal modeling and verification of routing protocols of ad hoc networks. We derive the key concepts that are vital in modeling ad hoc network protocols and then modify process algebra, appropriate for verifying protocols at network layer. This process algebra implements mobility behaviors of underlying infrastructure implicitly in the semantics of broadcastina. The semantics of broadcast communication also abstracts away the services provided by MAC layer.