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!
|
| Summary: | 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. |
|---|---|
| ISSN: | 1550-1477 |