AODVv2: Performance vs. Loop Freedom

作者: Mojgan Kamali , Massimo Merro , Alice Dal Corso

DOI: 10.1007/978-3-319-73117-9_24

关键词: Wireless ad hoc networkDistance-vector routing protocolStatistical modelComputer scienceLossy compressionLoop (topology)TopologyRouting protocolAd hoc On-Demand Distance Vector RoutingStatistical model checking

摘要: We compare two evolutions of the Ad-hoc On-demand Distance Vector (AODV) routing protocol, i.e. DYMO and AODVv2-16. In particular, we apply statistical model checking to investigate performance these protocols in terms routes established looping routes. Our modelling analysis are carried out by Uppaal Statistical Model Checker on 3\(\,\times \,\)3 grids, with possibly lossy communication.

参考文章(28)
Luca Battisti, Damiano Macedonio, Massimo Merro, Statistical Model Checking of a Clock Synchronization Protocol for Sensor Networks fundamentals of software engineering. ,vol. 8161, pp. 168- 182 ,(2013) , 10.1007/978-3-642-40213-5_11
Kedar S. Namjoshi, Richard J. Trefler, Loop Freedom in AODVv2 formal techniques for (networked and) distributed systems. pp. 98- 112 ,(2015) , 10.1007/978-3-319-19195-9_7
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner, Annabelle McIver, Marius Portmann, Wee Lum Tan, A process algebra for wireless mesh networks european symposium on programming. ,vol. 7211, pp. 295- 315 ,(2012) , 10.1007/978-3-642-28869-2_15
Ansgar Fehnker, Peter Höfner, Marius Portmann, Wee Lum Tan, Annabelle McIver, Rob van Glabbeek, A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV arXiv: Networking and Internet Architecture. ,(2013)
Ansgar Fehnker, Peter Höfner, Marius Portmann, Wee Lum Tan, Annabelle McIver, Rob van Glabbeek, Automated analysis of AODV using UPPAAL tools and algorithms for construction and analysis of systems. ,vol. 7214, pp. 173- 187 ,(2012) , 10.1007/978-3-642-28756-5_13
Mojgan Kamali, Peter Höfner, Maryam Kamali, Luigia Petre, Formal Analysis of Proactive, Distributed Routing Software Engineering and Formal Methods. pp. 175- 189 ,(2015) , 10.1007/978-3-319-22969-0_13
Gerd Behrmann, Alexandre David, Kim G. Larsen, A Tutorial on UPPAAL formal methods. pp. 200- 236 ,(2004) , 10.1007/978-3-540-30080-9_7
Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter, Formal verification of standards for distance vector routing protocols Journal of the ACM. ,vol. 49, pp. 538- 576 ,(2002) , 10.1145/581771.581775
Massimo Merro, Francesco Ballardin, Eleonora Sibilio, A timed calculus for wireless systems Theoretical Computer Science. ,vol. 412, pp. 6585- 6611 ,(2011) , 10.1016/J.TCS.2011.07.016
Rob van Glabbeek, Peter Höfner, Wee Lum Tan, Marius Portmann, Sequence numbers do not guarantee loop freedom: AODV can yield routing loops modeling analysis and simulation of wireless and mobile systems. pp. 91- 100 ,(2013) , 10.1145/2507924.2507943