A performability analysis of mobile wireless sensor networks with probabilistic model checking

This article presents a method to check the per-formability of mobile wireless sensor networks. After introducing this method based on formal methods, we apply it to check the performability of an application in a hospital context. A pilot application was deployed to check its properties. We propose to model some aspects of its specifications before checking them. We use a process calculus suitable for reliability and performance modelling of mobile systems. These models are then translated into the language of PRISM, a probabilistic model checker which enables checking of considered properties.