Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

Modelling and symmetry reduction of a target-tracking protocol using wireless sensor networks

Modelling and symmetry reduction of a target-tracking protocol using wireless sensor networks

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Add to cart
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)
Add to cart

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
IET Communications — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

  • Author(s): S. Bhatti 1 ; S. Memon 2 ; I.A. Jokhio 3 ; M.A. Memon 4
    • View affiliations
    • Affiliations: 1: Department of Software Engineering, Mehran University of Engineering and Technology, Jamshoro, Pakistan
      2: Department of Computer Systems Engineering, Mehran University of Engineering and Technology, Jamshoro, Pakistan
      3: Department of Software Engineering, Mehran University of Engineering and Technology, Jamshoro, Pakistan
      4: Department of Computer Science, Graduate School of Systems and Information Engineering, University of Tsukuba, Japan
  • Source: Volume 6, Issue 10, 3 July 2012, p. 1205 – 1211
    DOI:  10.1049/iet-com.2011.0246 , Print ISSN 1751-8628, Online ISSN 1751-8636
© The Institution of Engineering and Technology
Published

To achieve precise modelling of real-time systems stochastic behaviours are considered which lead towards probabilistic modelling. Probabilistic modelling has been successfully employed in wide array of application domains including, for example, randomised distributed algorithms, communication, security and power management protocols. This study is an improvement over our previous work, which was based on the probabilistic analysis of a cluster-based fault tolerant target-tracking protocol (FTTT) using only grid-based sensor nodes arrangement. Probabilistic modelling is chosen for the analysis of FTTT protocol to facilitate benefits of symmetry reduction in conjunction with modelling. It is believed that for the first time correctness of the simplified version of a target-tracking protocol is verified by developing its continuous-time Markov chain (CTMC) model using symbolic modelling language. The proposed probabilistic model of a target-tracking wireless sensor networks will help to analyse the phases of FTTT protocol on a limited scale with finite utilisation of time. There are three main contributions of this study; first consideration of synchronised events between the modules, second, random placement of sensor nodes is taken into account in addition to grid-based sensor node arrangement, third one is the reduction in state space size through symmetry reduction technique, which also facilitates to analyse a larger size network. Symmetry reduction on Probabilistic Symbolic Model (PRISM) checker models is performed by PRISM-symm and the generic representatives in PRISM (GRIP) tool. Modelling of FTTT protocol is proved better with the usage of PRISM-symm after comparing the results of PRISM model, PRISM-symm and GRIP.

Inspec keywords: probability; target tracking; Markov processes; telecommunication network reliability; protocols; wireless sensor networks; fault tolerance

Other keywords: continuous time Markov chain model; symmetry reduction; symbolic modelling language; real time systems stochastic behaviour; probabilistic modelling; grid based sensor node; PRISM; cluster based fault tolerant target tracking protocol; probabilistic analysis; wireless sensor networks; probabilistic symbolic model

Subjects: Protocols; Reliability; Markov processes; Wireless sensor networks

References

    1. 1)
      • Yuksel, E., Nielson, H.R., Nielson, F., Fruth, M., Kwiatkowska, M.: `Optimizing key updates in sensor networks', Proc. IEEE Sensors Applications Symp. (SAS'11), February 2011, p. 82–87.
    2. 2)
    3. 3)
      • Donaldson, A., Miller, A., Parker, D.: `Language-level symmetry reduction for probabilistic model checking', Proc. Sixth Int. Conf. on Quantitative Evaluation of Systems (QEST'09), IEEE Computer Society, September 2009, p. 289–298.
    4. 4)
      • Lluch-Lafuente, A., Edelkamp, S., Leue, S.: `Partial order reduction in directed model checking', Proc. Ninth Int. SPIN Workshop on Model Checking of Software, 2002, p. 112–127.
    5. 5)
      • Bertolini, C., Mota, A.: `Using probabilistic model checking to evaluate GUI testing techniques', Proc. 2009 Seventh IEEE Int. Conf. on Software Engineering and Formal Methods (SEFM), IEEE Computer Society, 23–27 November 2009, Washington, DC, p. 115–124.
    6. 6)
      • Chen, T., Kwiatkowska, M., Parker, D., Simaitis, A.: `Verifying team formation protocols with probabilistic model checking', Proc. 12th Int. Workshop on Computational Logic in Multi-Agent Systems (CLIMA XII 2011), July 2011, p. 190–297, (LNCS, 6814).
    7. 7)
      • Emerson, E., Trefler, R.: `From asymmetry to full symmetry: new techniques for symmetry reduction in model checking', Proc. Correct Hardware Design and Verification Methods (CHARME), 1999, p. 142–156, (ser. LNCS, 1703).
    8. 8)
      • Donaldson, A., Miller, A.: `Symmetry reduction for probabilistic model checking using generic representatives', Proc. Fourth Int. Symp. on Automated Technology for Verification and Analysis (ATVA'06), October 2006, p. 9–23, (LNCS, 4218).
    9. 9)
      • M. Duflot , M. Kwiatkowska , G. Norman , S. Gnesi , T. Margaria . (2010) Practical applications of probabilistic model checking to communication protocols, FMICS handbook on industrial critical systems.
    10. 10)
      • Lazos, L., Poovendran, R., Ritcey, J.A.: `Probabilistic detection of mobile targets in heterogeneous sensor networks', Proc. Sixth Int. Conf. on Information Processing in Sensor Networks, 25–27 April 2007, Cambridge, MA, USA, p. 519–528.
    11. 11)
      • Donaldson, A., Miller, A., Parker, D.: `GRIP: generic representatives in PRISM', Proc. Fourth Int. Conf. on Quantitative Evaluation of Systems (QEST'07), September 2007, p. 115–116.
    12. 12)
    13. 13)
      • Donaldson, A., Miller, A.: `Symmetry reduction for probabilistic systems', Proc. 12th Workshop on Automated Reasoning, 2005, p. 17–18.
    14. 14)
    15. 15)
    16. 16)
    17. 17)
      • Kwiatkowska, M., Norman, G., Parker, D.: `Advances and challenges of probabilistic model checking', Proc. 48th Annual Allerton Conf. on Communication, Control and Computing, October 2010, Invited paper.
    18. 18)
      • Bhatti, S., Xu, J., Memon, M.: `Model checking of a target tracking protocol for wireless sensor networks', Proc. Tenth Int. Conf. on Computer and Information Technology, 29 June–01 July 2010, Bradford, UK, p. 2867–2872.
    19. 19)
    20. 20)
      • Kwiatkowska, M., Norman, G., Parker, D.: `Symmetry reduction for probabilistic model checking', Proc. 18th Int. Conf. on Computer Aided Verification (CAV'06), August 2006, p. 234–248, (LNCS, 4144.
    21. 21)
      • Bhatti, S., Xu, J., Memon, M.: `Energy-aware fault-tolerant clustering scheme for target tracking wireless sensor networks', Proc. Seventh Int. Symp. on Wireless Communication Systems, York, The University of York, 19–22 September 2010, UK, p. 531–535.
    22. 22)
      • Ballarini, P., Miller, A.: `Model checking medium access control for sensor networks', Second Int. Symp. on Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2006, 15–19 November 2006, Paphos, Cyprus, p. 255–262.
    23. 23)
      • Kwiatkowska, M., Parker, D.: `Advances in probabilistic model checking', Proc. 2011 Marktoberdorf Summer School: Tools for Analysis and Verification of Software Safety and Security, IOS Press, 2012, To appear.
    24. 24)
      • ‘PRISM web site,’ www.prismmodelchecker.org.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-com.2011.0246
Loading

Related content

content/journals/10.1049/iet-com.2011.0246
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
Print this page
This is a required field
Please enter a valid email address