SCIRP Mobile Website
Paper Submission

Why Us? >>

  • - Open Access
  • - Peer-reviewed
  • - Rapid publication
  • - Lifetime hosting
  • - Free indexing service
  • - Free promotion service
  • - More citations
  • - Search engine friendly

Free SCIRP Newsletters>>

Add your e-mail address to receive free newsletters from SCIRP.

 

Contact Us >>

WhatsApp  +86 18163351462(WhatsApp)
   
Paper Publishing WeChat
Book Publishing WeChat
(or Email:book@scirp.org)

Article citations

More>>

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

has been cited by the following article:

  • 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.