TITLE:
A Quantitative Analysis of Collision Resolution Protocol for Wireless Sensor Network
AUTHORS:
Reema Patel, Dhiren Patel
KEYWORDS:
Wireless Sensor Network, Collision Resolution Protocol, Probabilistic Model Checking, Symmetry Reduction
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.8 No.8,
August
13,
2015
ABSTRACT: In this paper, we present formal analysis
of 2CS-WSN collision resolution protocol for wireless sensor networks using
probabilistic model checking. The 2CS-WSN protocol is designed to be used
during the contention phase of IEEE 802.15.4. In previous work on 2CS-WSN
analysis, authors formalized protocol description at abstract level by defining
counters to represent number of nodes in specific local state. On abstract
model, the properties specifying individual node behavior cannot be analyzed.
We formalize collision resolution protocol as a Markov Decision Process to
express each node behavior and perform quantitative analysis using
probabilistic model checker PRISM. The identical nodes induce symmetry in the
reachable state space which leads to redundant search over equivalent areas of
the state space during model checking. We use “ExplicitPRISMSymm” on-the-fly
symmetry reduction approach to prevent the state space explosion and thus
accommodate large number of nodes for analysis.