Formal Verification of Ad Hoc Network Routing Protocols

Main Article Content

Amandeep Verma


The conventional wireless network makes use of the base station, hardware, as a central entity. When no base station on hand or it is out of range, mobile nodes can still form a fully connected wireless network, accordingly called ad hoc mode. Ever since the initiative of ad hoc routing was regarded, an overabundance of protocols has surfaced, customized for a particular state. If a routing protocol does not achieve as projected, it is reduced quality of service. The routing protocol should be validated before deployment. A good way to confirm a protocol is to use formal verification techniques. This paper presents the various tools/techniques/languages used for formal modeling and verification of the ad hoc network routing protocols. It ranges from Petri nets, SPIN Model Checker, PROMELA, AVISPA, HLPSL, UPPAAL Model Checker, SDL and BAN logic.



Keywords: ad hoc networks, AVISPA, BAN Logic, formal verification, Petri nets, SDL, SPIN, UPPAAL


Download data is not yet available.

Article Details