A Quantitative Analysis of Collision Resolution Protocol for Wireless Sensor Network
- 1 Computer Engineering Department, NIT, Surat, India
- 2 Computer Engineering Department, NIT, Surat, India
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.
- Yick, J., Mukherjee, B. and Ghosal, D. (2008) Wireless Sensor Network Survey. Computer Networks, Science Direct, 52, 2292-2330. http://dx.doi.org/10.1016/j.comnet.2008.04.002
- Akyildiz, I.F., Weilian, S., Sankarasubramaniam, Y. and Cayirci, E. (2002) A Survey on Sensor Networks. IEEE Communications Magazine, 40, 102-114. http://dx.doi.org/10.1109/MCOM.2002.1024422
- Rawat, P., Singh, K., Chaouchi, H. and Bonnin, J. (2014) Wireless Sensor Networks: A Survey on Recent Developments and Potential Synergies. The Journal of Supercomputing, 68, 1-48. http://dx.doi.org/10.1007/s11227-013-1021-9
- Paterakis, M. and Papantoni-Kazakos, P. (1988) A Simple Window Random Access Algorithm with Advantageous Properties. Proceedings of the 7th Annual Joint Conference of the IEEE Computer and Communications Societies, Networks: Evolution or Revolution (INFOCOM’88), New Orleans, 27-31 March 1988, 907-915. http://dx.doi.org/10.1109/infcom.1988.13006
- (2006) IEEE Standard for Information Technology—Local and Metropolitan Area Networks—Specific Requirements—Part 15.4: Wireless Medium Access Control (MAC) and Physical Layer (PHY) Specifications for Low Rate Wireless Personal Area Networks (WPANs). IEEE Std 802.15.4-2006 (Revision of IEEE Std 802.15.4-2003), 1-320. http://dx.doi.org/10.1109/IEEESTD.2006.232110
- Hinton, A., Kwiatkowska, M., Norman, G. and Parker, D. (2006) PRISM: A Tool for Automatic Verification of Probabilistic Systems. Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), Vienna, 25 March-2 April 2006, 441-444. http://dx.doi.org/10.1007/11691372_29
- Rutten, J.J.M.M., Kwiatkowska, M., Norman, G. and Parker, D. (2004) Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series, American Mathematical Society, 23. http://qav.comlab.ox.ac.uk/bibitem.php?key=KNP04a
- Mateo, J.A., Macià, H., Ruiz, M.C., Calleja, J. and Royo, F. (2015) Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation. International Journal of Distributed Sensor Networks, 2015, Article ID: 285396. http://dx.doi.org/10.1155/2015/285396
- Patel, R., Patel, K. and Patel, D. (2015) ExplicitPRISMSymm: Symmetry Reduction Technique for Explicit Models in PRISM. Proceedings of the 12th Annual Conference on Theory and Applications of Models of Computation (TAMC’15), Singapore, 18-20 May 2015, 400-412. http://dx.doi.org/10.1007/978-3-319-17142-5_34