Abstract. The aim of this research is to enhance performance analysis of wireless networks based on simulation with formal performance analysis.

It is well-known that the performance of protocols for wireless networks, and their ability to tolerate faults arising due to the uncertainties underlying wireless communication, relies as much on the topology of the network as on the protocols' internal algorithms. Many general-purpose simulation tools however do not use realistic models of wireless communication, and indeed results of simulation experiments can differ widely between simulators and often bear scant relation to field experiments [7,6].

On the other hand, whilst model checking can supply more robust and exhaustive measures of performance, as for simulation, it is similarly flawed in that the details of the wireless communication are often overly simplified.

In this paper we propose a graphical specification style, which eases the study of the effect of topologies in performance analysis by visualising both the spatial characteristics of the network as well as critical measures of performance that they imply. Unlike other graphical visualisation tools, our proposal integrates both simulation using the novel Castalia simulator [3] as well as probabilistic model checking using PRISM [8], where we capture the effect of the topology by using probabilistic abstractions to model reception rates.