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

José Antonio Mateo | Zendy; Hermenegilda Macià | Zendy; M. Carmen Ruiz | Zendy; Javier Calleja | Zendy; Fernando Sancho Royo | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

José Antonio Mateo,

Hermenegilda Macià,

M. Carmen Ruiz,

Javier Calleja,

Fernando Sancho Royo

Publication year - 2015

Publication title -

international journal of distributed sensor networks

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.324

H-Index - 53

eISSN - 1550-1477

pISSN - 1550-1329

DOI - 10.1155/2015/285396

Subject(s) - computer science , correctness , probabilistic logic , model checking , markov chain , formalism (music) , wireless sensor network , algorithm , collision , theoretical computer science , formal verification , distributed computing , real time computing , programming language , computer network , artificial intelligence , machine learning , art , musical , visual arts

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research