Modelling and verifying the AODV routing protocol
作者： Peter Höfner , Marius Portmann , Wee Lum Tan , Rob Glabbeek
DOI: 10.1007/S00446-015-0262-7
关键词:
摘要: This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), recent process algebra which has been tailored modelling mobile ad networks and wireless mesh network protocols. Our formalisation models exact details core functionality AODV, such as route discovery, maintenance error handling. We demonstrate how can be used to reason about critical properties by providing detailed proofs loop freedom correctness.
uq.edu.au
springer.com
core.ac.uk
arxiv.org
acm.org
harvard.edu参考文章(49)
Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, Joachim Parrow, Broadcast Psi-calculi with an Application to Wireless Protocols Software Engineering and Formal Methods. pp. 74- 89 ,(2011) , 10.1007/978-3-642-24690-6_7
Peter Höfner, Peter Höfner, Timothy Bourke, Timothy Bourke, Robert J. van Glabbeek, Robert J. van Glabbeek, Showing invariance compositionally for a process algebra for network protocols interactive theorem proving. ,vol. 8558, pp. 144- 159 ,(2014) , 10.1007/978-3-319-08970-6_10
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
Robin Milner, Communication and Concurrency ,(1989)
Peter Höfner, Peter Höfner, Timothy Bourke, Timothy Bourke, Robert J. van Glabbeek, Robert J. van Glabbeek, A mechanized proof of loop freedom of the (untimed) AODV routing protocol automated technology for verification and analysis. ,vol. 8837, pp. 47- 63 ,(2014) , 10.1007/978-3-319-11936-6_5
Jens Chr. Godskesen, Observables for mobile and wireless broadcasting systems international conference on coordination models and languages. ,vol. 6116, pp. 1- 15 ,(2010) , 10.1007/978-3-642-13414-2_1
Sibusisiwe Chiyangwa, Marta Kwiatkowska, A Timing Analysis of AODV Lecture Notes in Computer Science. pp. 306- 321 ,(2005) , 10.1007/11494881_20
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)
Philippe Jacquet, Anis Laouiti, Pascale Minet, Laurent Viennot, Performance of Multipoint Relaying in Ad Hoc Mobile Routing Protocols international ifip tc networking conference. pp. 387- 398 ,(2002) , 10.1007/3-540-47906-6_31
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