@TechReport{	  it:2007-035,
  author	= {Mayank Saksena and Oskar Wibling and Bengt Jonsson},
  title		= {Graph Grammar Modeling and Verification of Ad Hoc Routing
		  Protocols},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2007},
  number	= {2007-035},
  month		= dec,
  note		= {Updated March 2008. Extended abstract to appear in proc.
		  14th Int. Conf. on Tools and Algorithms for the
		  Construction and Analysis of Systems (TACAS 2008).},
  abstract	= {We present a technique for modeling and automatic
		  verification of network protocols, based on graph
		  transformation. It is suitable for protocols with a
		  potentially unbounded number of nodes, in which the
		  structure and topology of the network is a central aspect,
		  such as routing protocols for ad hoc networks. Safety
		  properties are specified as a set of undesirable global
		  configurations. We verify that there is no undesirable
		  configuration which is reachable from an initial
		  configuration, by means of symbolic backward reachability
		  analysis. In general, the reachability problem is
		  undecidable. We implement the technique in a graph grammar
		  analysis tool, and automatically verify several interesting
		  non-trivial examples. Notably, we prove loop freedom for
		  the DYMO ad hoc routing protocol. DYMO is currently on the
		  IETF standards track, to potentially become an Internet
		  standard.}
}