Trustworthy Systems

A process algebra for wireless mesh networks


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



Macquarie University

Queensland University of Technology


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

    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        = {Proceedings of the 21st 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         = {},
    publisher        = {Springer},
    title            = {A Process Algebra for Wireless Mesh Networks},
    year             = {2012}