Oxford logo

Probabilistic Model Checking of Mobile Ad Hoc Network Protocols

Project details

Funded by: EPSRC (grant reference GR/S46727/01)

Dates: 2003-2006

Institutions: University of Birmingham


This proposal aims to investigate the foundations of modelling and analysis of mobile ad hoc network protocols, with the view to develop automated design validation methods capable of performance prediction and correctness assurance. Performance prediction, an essential factor when evaluating ad hoc network designs due to mobility, inherent delays in the underlying transmission mechanism and potential loss of interconnectivity, will be achieved through the novel probabilistic model checking techniques developed at Birmingham with EPSRC support. The functional correctness of the designs will be established by invoking verification via model checking, an automatic method that addresses the deficiencies of simulation by exploring all the possible executions of designs. The promise of model checking and probabilistic model checking, respectively, in the context of mobile ad hoc network protocols has already been successfully demonstrated through detecting errors in the AODV routing protocol specification and PRISM predictions obtained for stationary scenarios of delivery time for IEEE 802.11 and power management policies. The scientific challenge is to extend and adapt the methods to typical mobility models and metrics.


  • To investigate and formulate an appropriate model for mobile ad hoc networks with support for:
    • typical node mobility specifications and metrics;
    • main classes of routing protocols, e.g. link-state, on demand, etc;
    • selected low-level protocols such as BlueTooth or IEEE 802.11;
  • To extend and adapt probabilistic model checking methods to the mobility model, with the view to obtain automatic performance prediction and validation methods;
  • To develop prototypes as appropriate, depending on progress, and evaluate the outcome through case studies.


Further information