A Bigraphical Reactive Systems with Sharing for modeling Wireless Mesh Networks

Abstract

Recently, various types of wireless networks and mobile communication technologies have emerged; particularly the Wireless Mesh Networks (WMN) improving significantly the capacities of mobile communications. This paper aims to propose new insights on theoretical aspects of WMN by giving a novel modeling approach.We lean on formal methods to show how to define a precise semantics for WMN and how to formally analyze their routing protocols. We combine the logical reflection of Maude language and the hierarchical structure of the Bigraphical Reactive Systems (BRS) to provide an executable formal model for WMN. This model, called Bis-WMN specifies both the WMN topology and any behavior which may be observed during its routing process. Some inherent properties have been then checked with the LTL model checker of Maude.

Keywords

• WMNs
• Channels assignment
• Multi-path routing
• Bigraphical Reactive Systems
• Formal verification
• Model checker