Adaptive formal framework for WMN routing protocols

Wireless Mesh Networks (WMNs) are self-organising and self-healing wireless networks that provide support for broadband communication without requiring fixed infrastructure. A determining factor for the performance and reliability of such networks is the routing protocols applied in these networks. Formal modelling and verification of routing protocols are challenging tasks, often skipped by protocol designers. Despite some commonality between different models of routing protocols that have been published, these models are often tailored to a specific protocol which precludes easily comparing models. This paper presents an adaptive, generic and reusable framework as well as crucial generic properties w.r.t. system requirements, to model and verify WMN routing protocols. In this way, protocol designers can adapt the generic models based on protocol specifications and verify routing protocols prior to implementation. This model uses Uppaal SMC to identify the main common components of routing protocols, capturing timing aspect of protocols, communication between nodes, probabilities of message loss and link breakage, etc.