Analysis of Dynamic Process Networks

We formulate a method to compute global invariants of dynamic process networks, which can be used to model ad-hoc and sensor network protocols. In such networks, the inter-process connectivity as well as the set of active processes may be altered by an adversary at any point. The analysis combines elements of compositional reasoning, symmetry reduction, and abstraction. A compositional analysis is naturally less sensitive to network changes that occur far away from a focal point. We show how to couple this with a symmetry reduction based on similarities between local process neighborhoods. Together, they permit a small abstract network to represent arbitrary process neighborhoods from arbitrarily large networks. An invariant computed on the small network generalizes to a parametric invariant of the shape ``for all networks and all processes: property P holds of each process and its local neighborhood.'' We illustrate this method by showing how to compute useful invariants for a simple dining philosophers protocol, and the latest version of the ad-hoc routing protocol AODV (version 2).