Formal Methods for Performance Evaluation of Wireless Network Applications

Aim

The Formal Methods for Performance Evaluation of Wireless Network Applications (PEWNA) project ran from 2005 to 2008 and aimed at making advanced formal verification techniques available to designers of wireless sensor network applications and protocols.

What did the project achieve?

The primary aim was to increase awareness that the current design approach, which relies heavily on simulation, is inherently problematic. It can be unclear what is meant by a simulation. The project proved that a formal approach, based on rigid mathematics, can mitigate these problems.

The secondary aim was to develop tools and methods, specifically for the wireless domain, that offer formal techniques to non-experts in formal methods. A tangible outcome of the project is the front-end tool CaVi

Who will benefit?

The research is targeted to the developer and researcher working on protocols and applications in the wireless network domain.

What are the key features?

  • The project improved understanding of the ramifications of design in network protocols
  • It resulted in an automated tools for use in protocol design that can explore a wider range of network behaviour than is currently possible
  • It underpins the development of trusted wireless networks.

Progress update

The project finished in May 2008. The team members, in collaboration with other groups in NICTA are working on developing new project. The focus of the new project will be on protocols and the fundamental aspects of simulation.

Publications

  • A. Boulis, A. Fehnker, M. Fruth, and A. McIver. CaVi -- Simulation and Model Checking for Wireless Sensor Networks. Qest 2008. (pdf).
  • A. Fehnker, M. Fruth, and A. McIver. Graphical modelling for simulation and formal analysis of wireless network protocols. MeMot 2007. (pdf).
  • A. Fehnker, L. van Hoesel, and A. Mader. Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. IFM 2007. (pdf)
  • A. McIver and A. Fehnker. Formal techniques for the analysis of wireless networks, Isola 2006 (pdf).
  • A. McIver. Quantitative mu-calculus analysis of power management in wireless networks, ICTAC 2006 (pdf).
  • A. Fehnker and P. Gao. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. AdHocNow 2006 (pdf).

Project leader

Ansgar Fehnker

Research team

Athannasios Boulis, Ansgar Fehnker, Annabelle McIver

Collaboration with

Matthias Fruth (University of Birmingham), Angelika Mader (University of Twente), Sanjay Jha (UNSW)