Skip to main content


Formal analysis of proactive, distributed routing


Mojgan Kamali, Peter Hoefner, Maryam Kamali and Luigia Petre

Abo Akademi University



University of Liverpool


As (network) software is such an omnipresent component of contemporary mission-critical systems, formal analysis is required to provide the necessary certification or at least assurance for these sys- tems. In this paper we focus on modelling and analysing the Optimised Link State Routing (OLSR) protocol, a distributed, proactive routing protocol. It is recognised as one of the standard ad-hoc routing protocols for Wireless Mesh Networks (WMN). WMNs are instrumental in criti- cal systems, such as emergency response networks and smart electrical grids. We use the model checker Uppaal for analysing safety properties of OLSR as well as to point out a case of OLSR malfunctioning.

BibTeX Entry

    author           = {Kamali, Mojgan and Höfner, Peter and Kamali, Maryam and Petre, Luigia},
    month            = {sep},
    year             = {2015},
    title            = {Formal Analysis of Proactive, Distributed Routing},
    booktitle        = {Software Engineering and Formal Methods},
    pages            = {15},
    address          = {York, UK}