www.prismmodelchecker.org
[FMM07] A. Fehnker, M. Fruth and A. McIver. Graphical modelling for simulation and formal analysis of wireless network protocols. In Proc. Workshop on Methods, Models and Tools for Fault-Tolerance (MeMoT'07) at the 7th International Conference on Integrated Formal Methods (IFM'07), pages 80-87. Technical Report CS-TR-1032, University of Newcastle upon Tyne. July 2007. [pdf] [bib]
Downloads:  pdf pdf (178 KB)  bib bib
Links: [Google] [Google Scholar]
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.

Publications