MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis

  • Fatemeh Kazemeyni
  • Einar Broch Johnsen
  • Olaf Owe
  • Ilangko Balasingham
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


Wireless sensor networks (WSNs) consist of resource-constrained nodes; especially with respect to power. In most cases, the replacement of a dead node is difficult and costly. It is therefore crucial to minimize the total energy consumption of the network. Since the major consumer of power in WSNs is the data transmission process, we consider nodes which cooperate for data transmission in terms of groups. A group has a leader which collects data from the members and communicates with the outside of the group. We propose and formalize a model for data collection in which mobile entities, called data MULEs, are used to move between group leaders and collect data messages using short-range and low-power data transmission. We combine declarative and operational modeling. The declarative model abstractly captures behavior without committing to specific transitions by means of probability distributions, whereas the operational model is given as a concrete transition system in rewriting logic. The probabilistic, declarative model is not used to select transition rules, but to stochastically capture the result of applying rules. Technically, we use probabilistic rewriting logic and embed our models into PMaude, which gives us a simulation engine for the combined models. We perform statistical quantitative analysis based on repeated discrete-event simulations in Maude.


Sensor Network Sensor Node Wireless Sensor Network Model Check Data Message 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. ENTCS 153(2), 213–239 (2006)Google Scholar
  2. 2.
    Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless sensor networks: a survey. Computer Networks 38(4), 393–422 (2002)CrossRefGoogle Scholar
  3. 3.
    Anastasi, G., Conti, M., Di Francesco, M., Passarella, A.: Energy conservation in wireless sensor networks: A survey. Ad Hoc Networks 7(3), 537–568 (2009)CrossRefGoogle Scholar
  4. 4.
    Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Software Tools for Technology Transfer 14(1), 53–72 (2012)CrossRefGoogle Scholar
  5. 5.
    Bernardo, M., Gorrieri, R.: A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science 202(1-2), 1–54 (1998)MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  7. 7.
    Dario, I.A., Akyildiz, I.F., Pompili, D., Melodia, T.: Underwater acoustic sensor networks: Research challenges. Ad Hoc Networks 3(3), 257–279 (2005)CrossRefGoogle Scholar
  8. 8.
    Dong, J.S., Sun, J., Sun, J., Taguchi, K., Zhang, X.: Specifying and Verifying Sensor Networks: An Experiment of Formal Methods. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 318–337. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Ergen, S.C., Ergen, M., Koo, T.J.: Lifetime analysis of a sensor network with hybrid automata modelling. In: Proc. 1st ACM Int. Workshop on Wireless Sensor Networks and Applications, pp. 98–104 (2002)Google Scholar
  10. 10.
    Fehnker, A., Fruth, M., McIver, A.K.: Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Fault Tolerance. LNCS, vol. 5454, pp. 1–24. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Fehnker, A., van Hoesel, L., Mader, A.: Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Heinzelman, W.R., Chandrakasan, A., Balakrishnan, H.: Energy-efficient communication protocol for wireless microsensor networks. In: Proc. 33rd Hawaii Int. Conf. on System Sciences, vol. 8, p. 8020 (2000)Google Scholar
  13. 13.
    Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996)Google Scholar
  14. 14.
    Jain, S., Shah, R.C., Brunette, W., Borriello, G., Roy, S.: Exploiting mobility for energy efficient data collection in wireless sensor networks. Mobile Networks and Applications 11(3), 327–339 (2006)CrossRefGoogle Scholar
  15. 15.
    Katelman, M., Meseguer, J., Hou, J.C.: Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 150–169. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  16. 16.
    Kazemeyni, F., Johnsen, E.B., Owe, O., Balasingham, I.: Grouping Nodes in Wireless Sensor Networks Using Coalitional Game Theory. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE 2010. LNCS, vol. 6117, pp. 95–109. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  17. 17.
    Kumar, N., Sen, K., Meseguer, J., Agha, G.: Probabilistic Rewrite Theories: Unifying Models, Logics and Tools. Technical report UIUCDCS-R-2003-2347, Dept. of C. S., Univ. of Illinois at Urbana-Champaign (2003)Google Scholar
  18. 18.
    Kwiatkowska, M., Norman, G., Parker, D.: Quantitative analysis with the probabilistic model checker PRISM. ENTCS 153(2), 5–31 (2006)Google Scholar
  19. 19.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. ACM SIGMETRICS Performance Evaluation Review 36(4), 40–45 (2009)CrossRefGoogle Scholar
  20. 20.
    Lloret, J., Palau, C.E., Boronat, F., Tomás, J.: Improving networks using group-based topologies. Computer Communications 31(14), 3438–3450 (2008)CrossRefGoogle Scholar
  21. 21.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  22. 22.
    Muhammad, A., Azween, A.: Dynamic cluster based routing for underwater wireless sensor networks. In: ITSim 2010, 3 (June 2010)Google Scholar
  23. 23.
    Noori, M., Ardakani, M.: A probabilistic lifetime analysis for clustered wireless sensor networks. In: Proc. WCNC 2008, pp. 2373–2378 (2008)Google Scholar
  24. 24.
    Ölveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theoretical Computer Science 410(2-3), 254–280 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  25. 25.
    Di Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic Linda-Based Coordination Languages. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 120–140. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  26. 26.
    Pompili, D., Akyildiz, I.F.: Overview of networking protocols for underwater wireless communications. IEEE Communications Magazine 47(1), 97–102 (2009)CrossRefGoogle Scholar
  27. 27.
    Priami, C.: Stochastic π-calculus. Computer Journal 38(7), 578–589 (1995)CrossRefGoogle Scholar
  28. 28.
    Sen, K., Viswanathan, M., Agha, G.: VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems. In: Proc. 2nd Int. Conf. on the Quantitative Evaluation of Systems (QEST 2005), USA, p. 251 (2005)Google Scholar
  29. 29.
    Shah, R.C., Roy, S., Jain, S., Brunette, W.: Data mules: Modeling a three-tier architecture for sparse sensor networks. In: IEEE SNPA, pp. 30–41 (2003)Google Scholar
  30. 30.
    Tschirner, S., Xuedong, L., Yi, W.: Model-based validation of QoS properties of biomedical sensor networks. In: Int. Conf. on Embedded Software, pp. 69–78 (2008)Google Scholar
  31. 31.
    AlTurki, M., Meseguer, J.: PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Fatemeh Kazemeyni
    • 1
    • 2
  • Einar Broch Johnsen
    • 1
  • Olaf Owe
    • 1
  • Ilangko Balasingham
    • 2
  1. 1.Department of InformaticsUniversity of OsloNorway
  2. 2.The Intervention CenterOslo University HospitalOsloNorway

Personalised recommendations