Formal Analysis of Network Routing Protocols

Abstract

The use of wireless networks has been on the rise for some time now, from the ubiquitous smart phones and laptops in use everywhere, to sensor networks collecting large amounts of data. In this dissertation, we focus on contemporary wireless technologies, in particular Wireless Mesh Networks (WMNs): self-organising and self-healing wireless networks that support broadband communication without requiring any wired infrastructure. A significant factor for the reliability and flexibility of such networks is provided by the routing protocols. The current approaches used for analysing routing protocols, e.g., test-bed experiments and simulation techniques, are expensive, time consuming and resource-intensive. Additionally, these techniques cannot, in general, guarantee the reliability and flexibility of such systems. In order to address these challenges, the use of formal methods is growing, i.e., for the purpose of reasoning about wireless mesh network routing protocols. However, the mathematical foundation of formal techniques is considered as a challenging task for protocol designers, and therefore, this level of development (reliability and flexibility analysis) is often skipped. The objective of this dissertation is to study different routing protocols of wireless mesh networks using formal techniques as well as to propose a generic framework to formally model, analyse and verify such protocols as our ultimate goal. The proposed framework can help the protocol designers to verify their routing protocols prior to implementing them in real-case scenarios and to avoid consequent costs. We employ classical model checking (via the Uppaal tool), statistical model checking (via the Uppaal SMC tool) and theorem proving in Event-B (via the Rodin platform) to carry out our study and deal with both quantitative and qualitative analysis of such systems. Our generic and reusable framework is developed employing the Uppaal SMC as the tool support.