Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Modelling Link State Routing i...

Modelling Link State Routing in Event-B

Mojgan Kamali, Luigia Petre, Modelling Link State Routing in Event-B. In: Hai Wang, Mounir Mokhtari (Eds.), 21st International Conference on Engineering of Complex Computer Systems, ICECCS 2016, 207–210, IEEE Conference Publishing Services, 2016.

Abstract:

In this paper we present a stepwise formal development of the Optimised Link State Routing (OLSR) protocol in Event-B. OLSR is a proactive routing protocol which finds routes for different destinations in advance by exchanging control messages through the network. As a consequence, whenever a data packet is injected into the network can be delivered to a certain destination immediately. To achieve this, routing tables in OLSR are continuously updated, by following a rather complicated algorithm. By modelling OLSR in Event-B, we address the scalability problem of our previous work, and structure the OLSR complexity in five distinct abstraction layers. These layers are manageable to understand and to verify and are linked to each other by refinement. As Event-B is supported by a theorem proving platform (Rodin), we model and prove functional properties of OLSR in an automated and interactive manner, at a highly general level. Our approach can serve as a proof-of-concept to be adapted to modelling and verifying of the other routing protocols for large-scale networks.

BibTeX entry:

@INPROCEEDINGS{inpKaPe16a,
  title = {Modelling Link State Routing in Event-B},
  booktitle = {21st International Conference on Engineering of Complex Computer Systems, ICECCS 2016},
  author = {Kamali, Mojgan and Petre, Luigia},
  editor = {Wang, Hai and Mokhtari, Mounir},
  publisher = {IEEE Conference Publishing Services},
  pages = {207–210},
  year = {2016},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication