Funded by:
(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.