A Bigraphical Reactive Systems with Sharing for modeling Wireless Mesh Networks

Journal of King Saud University: Computer and Information Sciences

Faiza Belala¹  Rachida Boucebsi² 

[1] LIRE Laboratory, Constantine II University-Abdelhamid Mehri, Nouvelle ville Ali Mendjeli BP: 67A, Constantine, Algeria;Corresponding authors.;

关键词: WMNs;    Channels assignment;    Multi-path routing;    Bigraphical Reactive Systems;    Formal verification;    Model checker;   

DOI  :  

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown