Trustworthy Systems

A process algebra for wireless mesh networks

Authors

Ansgar Fehnker, Rob van Glabbeek, Peter Hoefner, Annabelle McIver, Marius Portmann and Wee Lum Tan

NICTA

UNSW

Macquarie University

Queensland University of Technology

Abstract

We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.

BibTeX Entry

  @inproceedings{Fehnker_GHMPT_12,
    address          = {Tallinn, Estonia},
    author           = {Fehnker, Ansgar and van Glabbeek, Robert and H\"ofner, Peter and McIver, Annabelle and Portmann,
                        Marius and Tan, Wee Lum},
    booktitle        = {European Symposium on Programming},
    editor           = {{Helmut Seidl}},
    issn             = {0302-9743},
    keywords         = {process algebra; wireless mesh networks; ad-hoc on-demand distance vector (aodv); routing protocols;
                        loop freedom},
    month            = mar,
    pages            = {295--315},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4801.pdf},
    publisher        = {Springer},
    title            = {A Process Algebra for Wireless Mesh Networks},
    year             = {2012}
  }

Download