| Title: | Modelling medium access control in IEEE 802.15.4 nonbeacon-enabled networks with probabilistic timed automata |
|---|
| Authors: | ID Kapus, Tatjana (Author) |
| Files: | Mobile_Information_Systems_2013_Kapus_Modelling_medium_access_control_in_IEEE_802.15.4_nonbeacon-enabled_networks_with_probabilistic_tim.pdf (2,25 MB) MD5: AFADA56129143B1D81843EEC82D1367C
https://www.hindawi.com/journals/misy/2013/732137/abs/
|
|---|
| Language: | English |
|---|
| Work type: | Scientific work |
|---|
| Typology: | 1.01 - Original Scientific Article |
|---|
| Organization: | FERI - Faculty of Electrical Engineering and Computer Science
|
|---|
| Abstract: | This paper concerns the formal modelling of medium access control in nonbeacon-enabled IEEE 802.15.4 wireless personal area networks with probabilistic timed automata supported by the PRISM probabilistic model checker. In these networks, the devices contend for the medium by executing an unslotted carrier sense multiple access with collision avoidance algorithm. In the literature, a model of a network which consists of two stations sending data to two different destination stations is introduced. We have improved this model and, based on it, we propose two ways of modelling a network with an arbitrary number of sending stations, each having its own destination. We show that the same models are valid representations of a star-shaped network with an arbitrary number of stations which send data to the same destination station. We also propose how to model such a network if some of the sending stations are not within radio range of the others, i.e. if they are hidden. We present some results obtained for these models by probabilistic model checking using PRISM. |
|---|
| Keywords: | wireless personal area network, medium access control, hidden station, formal specification, probabilistic model checking |
|---|
| Publication status: | Published |
|---|
| Publication version: | Version of Record |
|---|
| Number of pages: | str. 157-188 |
|---|
| Numbering: | Letn. 9, št. 2 |
|---|
| PID: | 20.500.12556/DKUM-66217  |
|---|
| ISSN: | 1574-017X |
|---|
| UDC: | 659.2 |
|---|
| ISSN on article: | 1574-017X |
|---|
| COBISS.SI-ID: | 16807958  |
|---|
| DOI: | 10.3233/MIS-130160  |
|---|
| NUK URN: | URN:SI:UM:DK:NTFJRHOD |
|---|
| Publication date in DKUM: | 15.06.2017 |
|---|
| Views: | 1371 |
|---|
| Downloads: | 395 |
|---|
| Metadata: |  |
|---|
| Categories: | Misc.
|
|---|
|
:
|
Copy citation |
|---|
| | | | Average score: | (0 votes) |
|---|
| Your score: | Voting is allowed only for logged in users. |
|---|
| Share: |  |
|---|
Hover the mouse pointer over a document title to show the abstract or click
on the title to get all document metadata. |