Oxford logo
[GMR+13] L. Gallina, A. Marin, S. Rossi, T. Han and M. Kwiatkowska. A Process-Algebraic Framework for Estimating the Energy Consumption in Ad-hoc Wireless Sensor Networks. In Proc. 16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM'13), pages 255-262, ACM. November 2013. [pdf] [bib]
Downloads:  pdf pdf (706 KB)  bib bib
Abstract. We present a framework for modelling ad-hoc Wireless Sensor Networks (WSNs) and studying both their connectivity properties and their performance in terms of energy consumption, throughput and other relevant indices. Our framework is based on a probabilistic process calculus where system executions are driven by Markovian probabilistic schedulers, allowing us to translate process terms into discrete time Markov chains (DTMCs) and use the probabilistic model checker PRISM to automatically evaluate/estimate the connectivity properties and the energy costs of the networks. To the best of our knowledge, this is the first work that proposes a unique framework for studying qualitative (e.g., by proving the equivalence of components or the correctness of a behaviour) and quantitative aspects of WSNs using a tool that allows both exact and approximate (via Monte Carlo simulation) analyses. We demonstrate our framework at work by considering different communication strategies based on gossip routing protocols, for a typical topology and a mobility scenario.