Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation

José A. Mateo, Hermenegilda MaciÃ, M. Carmen Ruiz, Javier Calleja and Fernando Royo

International Journal of Distributed Sensor Networks, 2015, vol. 11, issue 5, 285396

Abstract: 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.

Date: 2015
References: Add references at CitEc
Citations:

Downloads: (external link)
https://journals.sagepub.com/doi/10.1155/2015/285396 (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:sae:intdis:v:11:y:2015:i:5:p:285396

DOI: 10.1155/2015/285396

Access Statistics for this article

More articles in International Journal of Distributed Sensor Networks
Bibliographic data for series maintained by SAGE Publications ().