Formal Verification of a New Version of AOMDV in ad hoc Network

In ad hoc networks like MANET the topology change frequently and interferences problems are inevitable in many cases, as a result link failures can arise. Unfortunately, traditional routing algorithms are no more suitable for this kind of networks especially in case of using a single path routing schemes. In order to overcome this problem, multipath routing approach is proposed where in some cases as an extension of the traditional routing algorithms. Our aim in this paper is to propose a formal study based on model checking to formally verify an enhancement version of AOMDV. In this new version we have added new functionalities in ROUTE DISCOVERY and ROUTE MAINTENANCE to achieve energy efficiency, packet overhead minimization and latency reduction.