Path: Top -> Journal -> Jurnal Internasional -> King Saud University -> 2020 -> Volume 32, Issue 9, November
A Bigraphical Reactive Systems with Sharing for modeling Wireless Mesh Networks
Oleh : Rachida Boucebsi, Faiza Belala, King Saud University
Dibuat : 2021-08-14, dengan 0 file
Keyword : WMNs, Channels assignment, Multi-path routing, Bigraphical Reactive Systems, Formal verification, Model checker
Url : http://www.sciencedirect.com/science/article/pii/S1319157818303215
Sumber pengambilan dokumen : Web
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.
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.
Beri Komentar ?#(0) | Bookmark
| Properti | Nilai Properti |
|---|---|
| ID Publisher | gdlhub |
| Organisasi | King Saud University |
| Nama Kontak | Herti Yani, S.Kom |
| Alamat | Jln. Jenderal Sudirman |
| Kota | Jambi |
| Daerah | Jambi |
| Negara | Indonesia |
| Telepon | 0741-35095 |
| Fax | 0741-35093 |
| E-mail Administrator | elibrarystikom@gmail.com |
| E-mail CKO | elibrarystikom@gmail.com |
Print ...
Kontributor...
- Editor: Calvin