Seminar 13 Feb, 2012
Formal Methods for Wireless Mesh Networks
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the ``time-to-market'' for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks. In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the ``time-to-market'' for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks. In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
