A Quantitative Analysis of Collision Resolution Protocol for Wireless Sensor Network


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.

Share and Cite:

Patel, R. and Patel, D. (2015) A Quantitative Analysis of Collision Resolution Protocol for Wireless Sensor Network. Journal of Software Engineering and Applications, 8, 361-371. doi: 10.4236/jsea.2015.88036.

Conflicts of Interest

The authors declare no conflicts of interest.


[1] 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
[2] Akyildiz, I.F., Weilian, S., Sankarasubramaniam, Y. and Cayirci, E. (2002) A Survey on Sensor Networks. IEEE Communications Magazine, 40, 102-114.
[3] 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.
[4] 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
[5] (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.
[6] 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
[7] 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
[8] 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
[9] 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.
[10] Dave Parker, G.N. and Kwiatkowska, M. PRISM Case Studies.
[11] Katoen, J.P. (2010) Advances in Probabilistic Model Checking. Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’10), Madrid, 17-19 January 2010, 25-25. http://dx.doi.org/10.1007/978-3-642-11319-2_5
[12] Kwiatkowska, M., Norman, G. and Parker, D. (2002) PRISM: Probabilistic Symbolic Model Checker. Proceedings of the 12th International Conference on Computer Performance Evaluation: Modelling Techniques and Tools (TOOLS’02), London, 14-17 April 2002, 200-204.
[13] Fujita, M., McGeer, P.C. and Yang, J.C.Y. (1997) Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation. Formal Methods in System Design, 10, 149-169.
[14] Sistla, P. (2004) Employing Symmetry Reductions in Model Checking. Computer Languages, Systems and Structures, 30, 99-137. http://dx.doi.org/10.1016/j.cl.2004.02.002
[15] Miller, A., Donaldson, A. and Calder, M. (2006) Symmetry in Temporal Logic Model Checking. ACM Computing Surveys, 38, Article No. 8. http://dx.doi.org/10.1145/1132960.1132962
[16] Wahl, T., and Donaldson, A.F. (2010) Replication and Abstraction: Symmetry in Automated Formal Verification. Sym- metry, 2, 799-847. http://dx.doi.org/10.3390/sym2020799
[17] Kwiatkowska, M., Norman, G. and Parker, D. (2006) Symmetry Reduction for Probabilistic Model Checking. Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06), Seattle, 17-20 August 2006, 234-248. http://dx.doi.org/10.1007/11817963_23
[18] Royo, F., Lopez-Guerrero, M., Orozco-Barbosa, L. and Olivares, T. (2009) 2C-WSN: A Configuration Protocol Based on TDMA Communications over WSN. Proceedings of the 28th IEEE Conference on Global Telecommunications (GLOBECOM’09), Honolulu, 30 November-4 December 2009, 4057-4062.
[19] Pnueli, A., Xu, J. and Zuck, L.D. (2002) Liveness with (0, 1, Infty)-Counter Abstraction. Proceedings of the 14th International Conference on Computer Aided Verification (CAV’02), Denmark, July 27-31 2002, 107-122. http://dx.doi.org/10.1007/3-540-45657-0_9
[20] Ballarini, P. and Miller, A. (2006) Model Checking Medium Access Control for Sensor Networks. Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), Paphos, 15-19 November 2006, 255-262.

Copyright © 2022 by authors and Scientific Research Publishing Inc.

Creative Commons License

This work and the related PDF file are licensed under a Creative Commons Attribution 4.0 International License.