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.