@PhDThesis{	  itlic:2005-004,
  author	= {Oskar Wibling},
  title		= {Ad Hoc Routing Protocol Validation},
  school	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2005},
  number	= {2005-004},
  type		= {Licentiate thesis},
  month		= sep,
  day		= {23},
  abstract	= {We explore and evaluate methods for validation of ad hoc
		  routing protocols which are used to set up forwarding paths
		  in spontaneous networks of mobile devices. The focus is
		  automatic formal verification but we also make an initial
		  account of a protocol performance comparison using
		  structured live testing. State explosion is a major problem
		  in algorithmic verification of systems with concurrently
		  executing components. We comment on some of the best
		  reduction methods and their applicability to our work. For
		  reactively operating ad hoc routing protocols we provide a
		  broadcast abstraction which enables us to prove correct
		  operation of the Lightweight Underlay Network Ad hoc
		  Routing protocol (LUNAR) in scenarios of realistic size.
		  Our live testing effort has thus far uncovered significant
		  problems in the inter-operation between TCP and ad hoc
		  routing protocols. Severe performance degradation results
		  in networks of just a few nodes when very little mobility
		  is introduced. This indicates that verification for smaller
		  network sizes is also interesting since those
		  configurations may be the only useful ones for certain
		  types of applications.}
}