Modeling and verifying the OLSR protocol using Uppaal

Abstract

Wireless Mesh Networks (WMNs) are a popular technology due to their exibility andself-organizing nature that provide support for broadband communication. They areused in a wide range of application areas, such as public transportation, tunnels, realtime racing car telemetry and emergency response communication. Route _nding andmaintenance, two important factors determining the performance of such networks,are provided using routing algorithms. The Optimized Link State Routing (OLSR)protocol is an example of such algorithms which is used in this study.One issue about this protocol is that its speci_cation is in English that may causeambiguities or di_erent interpretations. The _rst contribution of this project is thedevelopment of a formal and unambiguous model of OLSR and its main functionalitiesusing timed automata as our formal speci_cation language. The second contributionof the project is a precise analysis of OLSR using the model checker Uppaal. By acareful automated analysis with Uppaal, the project shows a complementary approachto classical techniques, such as test-bed experiments and simulation.One overall goal of this study is the demonstration that automated, formal andrigorous analysis of real-world protocols is possible and can be achieved in a rathershort period of time. Our model covers all core components of OLSR and abstractsfrom the optional features. At the moment, the project analyses fundamental behaviorsuch as packet delivery; the model guarantees that a packet which is injected into anetwork is _nally delivered at the destination. Moreover, the study veri_es that nodesin the network can _nd shortest paths to other nodes.