Ad hoc networks are widely used for unmanaged and decentralized operations. Mobile ad hoc networks (MANETs) and wireless sensor networks are examples of ad hoc networks used for supporting self-configured and non-monitored services such as network routing and surveillance.

We developed the ω-calculus, a process-algebraic framework for formally modeling and reasoning about ad hoc networks and their protocols. The ω-calculus naturally captures essential characteristics of MANETs, including the ability of a MANET node to broadcast a message to any other node within its physical transmission range (and no others), and to move in and out of the transmission range of other nodes in the network. A key feature of the ω-calculus is the separation of a node's communication and computational behavior, described by an ω-process, from the description of its physical transmission range, referred to as an ω-process interface. The ω-calculus uses the notion of groups to model local broadcast-based communication, and separates the description of the actions of a protocol (called processes) from that of the network topology (specified by sets of groups, called interfaces of processes). As a result, the problems of verifying reachability properties and bisimilarity are decidable for a large class of omega calculus specifications (even in the presence of arbitrary node movement).

Ad hoc network protocols pose a unique verification problem called instance explosion because an AHN, with a fixed number of nodes, can assume exponential number of topologies. We have developed an automata-theoretic framework, based on key features of the omega-calculus, for the verification of ad hoc network protocols over unknown network topologies. Instance explosion is mitigated by using constraints to represent sets of topologies. A corresponding symbolic verification algorithm can efficiently infer the set of topologies for which an AHN protocol possesses a given correctness property.

We have also developed a partial model checker for parameterized systems of omega-calculus nodes. For a node M in an n-node system and a given formula ϕ, the partial model checker treats M as a property transformer, inferring the formula Π( M)(ϕ) that must hold in the (n-1)-node system with M removed. Our technique is such that n may be infinite, thereby supporting the verification of infinite families of processes.