Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol

Kaylash Chaudhary, Ansgar Fehnker, Vinay Mehta

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)

Abstract

This paper considers on a network routing protocol known as Better Approach to Mobile Ad hoc Networks (B.A.T.M.A.N.). The protocol serves two aims: first, to discover all bidirectional links, and second, to identify the best-next-hop for every other node in the network. A key element is that each node will flood the network at regular intervals with so-called originator messages.
This paper describes in detail a formalisation of the B.A.T.M.A.N. protocol. This exercise revealed several ambiguities and inconsistencies in the RFC. We developed two models. The first implements, if possible, a literal reading of the RFC, while the second model tries to be closer to the underlying concepts. The alternative model is in some places less restrictive, and rebroadcasts more often when it helps route discovery, and will on the other hand drop more messages that might interfere with the process.

We verify for a basic untimed model that both interpretations ensure loop-freedom, bidirectional link discovery, and route-discovery. We use simulation of a timed model to compare the performance and found that both models are comparable when it comes to the time and number of messages needed for discovering routes. However, the alternative model identifies a significantly lower number of suboptimal routes, and thus improves on the literal interpretation of the RFC.
Original languageEnglish
Title of host publicationProceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017
Subtitle of host publicationUppsala, Sweden, 29th April 2017
EditorsHolger Hermanns, Peter Höfner
PublisherEPTCS
Pages53-65
Number of pages13
DOIs
Publication statusPublished - 2017
Event2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017 - Uppsala, Sweden
Duration: 29 Apr 201729 Apr 2017
Conference number: 2
http://mars-workshop.org/mars2017/

Publication series

NameElectronic Proceedings in Theoretical Computer Science (EPTCS)
PublisherEPTCS
Volume244
ISSN (Print)2075-2180

Conference

Conference2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017
Abbreviated titleMARS
CountrySweden
CityUppsala
Period29/04/1729/04/17
Internet address

Fingerprint

Mobile ad hoc networks
Network protocols
Network routing
Routing protocols

Cite this

Chaudhary, K., Fehnker, A., & Mehta, V. (2017). Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol. In H. Hermanns, & P. Höfner (Eds.), Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017: Uppsala, Sweden, 29th April 2017 (pp. 53-65). (Electronic Proceedings in Theoretical Computer Science (EPTCS); Vol. 244). EPTCS. https://doi.org/10.4204/EPTCS.244.3
Chaudhary, Kaylash ; Fehnker, Ansgar ; Mehta, Vinay. / Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol. Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017: Uppsala, Sweden, 29th April 2017. editor / Holger Hermanns ; Peter Höfner. EPTCS, 2017. pp. 53-65 (Electronic Proceedings in Theoretical Computer Science (EPTCS)).
@inproceedings{f21c301cdf694c2f9802cb7d400fc46e,
title = "Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol",
abstract = "This paper considers on a network routing protocol known as Better Approach to Mobile Ad hoc Networks (B.A.T.M.A.N.). The protocol serves two aims: first, to discover all bidirectional links, and second, to identify the best-next-hop for every other node in the network. A key element is that each node will flood the network at regular intervals with so-called originator messages.This paper describes in detail a formalisation of the B.A.T.M.A.N. protocol. This exercise revealed several ambiguities and inconsistencies in the RFC. We developed two models. The first implements, if possible, a literal reading of the RFC, while the second model tries to be closer to the underlying concepts. The alternative model is in some places less restrictive, and rebroadcasts more often when it helps route discovery, and will on the other hand drop more messages that might interfere with the process.We verify for a basic untimed model that both interpretations ensure loop-freedom, bidirectional link discovery, and route-discovery. We use simulation of a timed model to compare the performance and found that both models are comparable when it comes to the time and number of messages needed for discovering routes. However, the alternative model identifies a significantly lower number of suboptimal routes, and thus improves on the literal interpretation of the RFC.",
author = "Kaylash Chaudhary and Ansgar Fehnker and Vinay Mehta",
year = "2017",
doi = "10.4204/EPTCS.244.3",
language = "English",
series = "Electronic Proceedings in Theoretical Computer Science (EPTCS)",
publisher = "EPTCS",
pages = "53--65",
editor = "Holger Hermanns and Peter H{\"o}fner",
booktitle = "Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017",

}

Chaudhary, K, Fehnker, A & Mehta, V 2017, Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol. in H Hermanns & P Höfner (eds), Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017: Uppsala, Sweden, 29th April 2017. Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 244, EPTCS, pp. 53-65, 2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017, Uppsala, Sweden, 29/04/17. https://doi.org/10.4204/EPTCS.244.3

Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol. / Chaudhary, Kaylash; Fehnker, Ansgar ; Mehta, Vinay.

Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017: Uppsala, Sweden, 29th April 2017. ed. / Holger Hermanns; Peter Höfner. EPTCS, 2017. p. 53-65 (Electronic Proceedings in Theoretical Computer Science (EPTCS); Vol. 244).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol

AU - Chaudhary, Kaylash

AU - Fehnker, Ansgar

AU - Mehta, Vinay

PY - 2017

Y1 - 2017

N2 - This paper considers on a network routing protocol known as Better Approach to Mobile Ad hoc Networks (B.A.T.M.A.N.). The protocol serves two aims: first, to discover all bidirectional links, and second, to identify the best-next-hop for every other node in the network. A key element is that each node will flood the network at regular intervals with so-called originator messages.This paper describes in detail a formalisation of the B.A.T.M.A.N. protocol. This exercise revealed several ambiguities and inconsistencies in the RFC. We developed two models. The first implements, if possible, a literal reading of the RFC, while the second model tries to be closer to the underlying concepts. The alternative model is in some places less restrictive, and rebroadcasts more often when it helps route discovery, and will on the other hand drop more messages that might interfere with the process.We verify for a basic untimed model that both interpretations ensure loop-freedom, bidirectional link discovery, and route-discovery. We use simulation of a timed model to compare the performance and found that both models are comparable when it comes to the time and number of messages needed for discovering routes. However, the alternative model identifies a significantly lower number of suboptimal routes, and thus improves on the literal interpretation of the RFC.

AB - This paper considers on a network routing protocol known as Better Approach to Mobile Ad hoc Networks (B.A.T.M.A.N.). The protocol serves two aims: first, to discover all bidirectional links, and second, to identify the best-next-hop for every other node in the network. A key element is that each node will flood the network at regular intervals with so-called originator messages.This paper describes in detail a formalisation of the B.A.T.M.A.N. protocol. This exercise revealed several ambiguities and inconsistencies in the RFC. We developed two models. The first implements, if possible, a literal reading of the RFC, while the second model tries to be closer to the underlying concepts. The alternative model is in some places less restrictive, and rebroadcasts more often when it helps route discovery, and will on the other hand drop more messages that might interfere with the process.We verify for a basic untimed model that both interpretations ensure loop-freedom, bidirectional link discovery, and route-discovery. We use simulation of a timed model to compare the performance and found that both models are comparable when it comes to the time and number of messages needed for discovering routes. However, the alternative model identifies a significantly lower number of suboptimal routes, and thus improves on the literal interpretation of the RFC.

U2 - 10.4204/EPTCS.244.3

DO - 10.4204/EPTCS.244.3

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science (EPTCS)

SP - 53

EP - 65

BT - Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017

A2 - Hermanns, Holger

A2 - Höfner, Peter

PB - EPTCS

ER -

Chaudhary K, Fehnker A, Mehta V. Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol. In Hermanns H, Höfner P, editors, Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2017: Uppsala, Sweden, 29th April 2017. EPTCS. 2017. p. 53-65. (Electronic Proceedings in Theoretical Computer Science (EPTCS)). https://doi.org/10.4204/EPTCS.244.3