Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation
A novel collision resolution algorithm for wireless sensor networks is formally analysed via probabilistic model checking. The algorithm called 2CS-WSN is specifically designed to be used during the contention phase of IEEE 802.15.4. Discrete time Markov chains (DTMCs) have been proposed as modellin...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2015-05-01
|
| Series: | International Journal of Distributed Sensor Networks |
| Online Access: | https://doi.org/10.1155/2015/285396 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832547259100692480 |
|---|---|
| author | José A. Mateo Hermenegilda Macià M. Carmen Ruiz Javier Calleja Fernando Royo |
| author_facet | José A. Mateo Hermenegilda Macià M. Carmen Ruiz Javier Calleja Fernando Royo |
| author_sort | José A. Mateo |
| collection | DOAJ |
| description | A novel collision resolution algorithm for wireless sensor networks is formally analysed via probabilistic model checking. The algorithm called 2CS-WSN is specifically designed to be used during the contention phase of IEEE 802.15.4. Discrete time Markov chains (DTMCs) have been proposed as modelling formalism and the well-known probabilistic symbolic model checker PRISM is used to check some correctness properties and different operating modes and, furthermore, to collect some performance measures. Thus, all the benefits of formal verification and simulation are gathered. These correctness properties as well as practical and relevant scenarios for the real world have agreed with the algorithm designers. |
| format | Article |
| id | doaj-art-f13da57a2d8247caa1a97165bf9f84fe |
| institution | Kabale University |
| issn | 1550-1477 |
| language | English |
| publishDate | 2015-05-01 |
| publisher | Wiley |
| record_format | Article |
| series | International Journal of Distributed Sensor Networks |
| spelling | doaj-art-f13da57a2d8247caa1a97165bf9f84fe2025-02-03T06:45:32ZengWileyInternational Journal of Distributed Sensor Networks1550-14772015-05-011110.1155/2015/285396285396Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks SimulationJosé A. MateoHermenegilda MaciàM. Carmen RuizJavier CallejaFernando RoyoA novel collision resolution algorithm for wireless sensor networks is formally analysed via probabilistic model checking. The algorithm called 2CS-WSN is specifically designed to be used during the contention phase of IEEE 802.15.4. Discrete time Markov chains (DTMCs) have been proposed as modelling formalism and the well-known probabilistic symbolic model checker PRISM is used to check some correctness properties and different operating modes and, furthermore, to collect some performance measures. Thus, all the benefits of formal verification and simulation are gathered. These correctness properties as well as practical and relevant scenarios for the real world have agreed with the algorithm designers.https://doi.org/10.1155/2015/285396 |
| spellingShingle | José A. Mateo Hermenegilda Macià M. Carmen Ruiz Javier Calleja Fernando Royo Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation International Journal of Distributed Sensor Networks |
| title | Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation |
| title_full | Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation |
| title_fullStr | Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation |
| title_full_unstemmed | Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation |
| title_short | Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation |
| title_sort | probabilistic model checking one step forward in wireless sensor networks simulation |
| url | https://doi.org/10.1155/2015/285396 |
| work_keys_str_mv | AT joseamateo probabilisticmodelcheckingonestepforwardinwirelesssensornetworkssimulation AT hermenegildamacia probabilisticmodelcheckingonestepforwardinwirelesssensornetworkssimulation AT mcarmenruiz probabilisticmodelcheckingonestepforwardinwirelesssensornetworkssimulation AT javiercalleja probabilisticmodelcheckingonestepforwardinwirelesssensornetworkssimulation AT fernandoroyo probabilisticmodelcheckingonestepforwardinwirelesssensornetworkssimulation |