Formal verification of MPR selection algorithm in the OLSR protocol

OLSR (Optimized Link State Routing) is a proactive routing protocol dedicated to MANET networks (Mobile Ad hoc Network) for establishing paths between network nodes. The operation of this protocol is mainly based on the MPR (Multi Point Relay) selection technique in order to reduce the traffic load of the network and also to minimize the path to the destination. The purpose of this paper focuses on the modeling under the UPPAAL (a tool that implements the model-checking technology for the verification of the network protocols behavior) to verify a set of properties of the MPR selection algorithm using the statistical model checking.