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 called2CS-WSNis 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.