Abstract
This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc On-Demand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.
| Original language | English |
|---|---|
| Title of host publication | Programming Languages and Systems |
| Subtitle of host publication | 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings |
| Editors | Peter Thiemann |
| Place of Publication | Berlin, Heidelberg |
| Publisher | Springer Berlin Heidelberg |
| Pages | 95-122 |
| Number of pages | 28 |
| ISBN (Electronic) | 978-3-662-49498-1 |
| ISBN (Print) | 978-3-662-49497-4 |
| DOIs | |
| Publication status | Published - 21 Mar 2016 |
| Event | 25th European Symposium on Programming 2016 - Eindoven, Netherlands Duration: 4 Apr 2016 → 7 Aug 2022 Conference number: 25 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Berlin, Heidelberg |
| Volume | 9632 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Symposium
| Symposium | 25th European Symposium on Programming 2016 |
|---|---|
| Abbreviated title | ESOP 2016 |
| Country/Territory | Netherlands |
| City | Eindoven |
| Period | 4/04/16 → 7/08/22 |