Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. ENTCS 153(2), 213–239 (2006)
Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless sensor networks: a survey. Computer Networks 38(4), 393–422 (2002)
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)
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)
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)
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)
Dario, I.A., Akyildiz, I.F., Pompili, D., Melodia, T.: Underwater acoustic sensor networks: Research challenges. Ad Hoc Networks 3(3), 257–279 (2005)
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)
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)
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)
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)
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)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996)
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)
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)
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)
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)
Kwiatkowska, M., Norman, G., Parker, D.: Quantitative analysis with the probabilistic model checker PRISM. ENTCS 153(2), 5–31 (2006)
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)
Lloret, J., Palau, C.E., Boronat, F., Tomás, J.: Improving networks using group-based topologies. Computer Communications 31(14), 3438–3450 (2008)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)
Muhammad, A., Azween, A.: Dynamic cluster based routing for underwater wireless sensor networks. In: ITSim 2010, 3 (June 2010)
Noori, M., Ardakani, M.: A probabilistic lifetime analysis for clustered wireless sensor networks. In: Proc. WCNC 2008, pp. 2373–2378 (2008)
Ö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)
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)
Pompili, D., Akyildiz, I.F.: Overview of networking protocols for underwater wireless communications. IEEE Communications Magazine 47(1), 97–102 (2009)
Priami, C.: Stochastic π-calculus. Computer Journal 38(7), 578–589 (1995)
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)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kazemeyni, F., Johnsen, E.B., Owe, O., Balasingham, I. (2012). MULE-Based Wireless Sensor Networks: Probabilistic Modeling and Quantitative Analysis. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)