Trustworthy Systems

Formal analysis of proactive, distributed routing

Authors

Mojgan Kamali, Peter Hoefner, Maryam Kamali and Luigia Petre

Abo Akademi University

NICTA

UNSW

University of Liverpool

Abstract

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

  @inproceedings{Kamali_HKP_15,
    address          = {York, UK},
    author           = {Kamali, Mojgan and H\"ofner, Peter and Kamali, Maryam and Petre, Luigia},
    booktitle        = {Software Engineering and Formal Methods},
    month            = sep,
    pages            = {15},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8831.pdf},
    title            = {Formal Analysis of Proactive, Distributed Routing},
    year             = {2015}
  }

Download