Testing Probabilistic Wireless Networks

We develop a probabilistic process calculus for modelling ad hoc wireless networks with static topology. We present a theory of composition for wireless networks, which we take as the starting point for developing a probabilistic generalisation of Hennessy and de Nicola may/must testing preorders. We present an extensional semantics for networks which we use to define the simulation and the novel deadlock simulation preorders; we prove that these are sound with respect to the may and must testing relations, respectively. However, the developed proof methods are not complete; we show an example of two networks which are may-testing related, but not simulation related, and we argue that the extensional semantics we developed cannot induce a sound and complete proof principle for the testing preorders. Finally, we show the usefulness of our proof techniques by proving the correct behaviour of a probabilistic routing protocol with respect to a formal specification.