With PQDT Open, you can read the full text of open access dissertations and theses free of charge.
About PQDT Open
Search
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.
Advisor: | Ramakrishnan, C. R., Smolka, Scott A. |
Commitee: | |
School: | State University of New York at Stony Brook |
School Location: | United States -- New York |
Source: | DAI-B 71/04, Dissertation Abstracts International |
Source Type: | DISSERTATION |
Subjects: | Computer science |
Keywords: | Ad hoc networks, Formal verification, MANETs, Omega calculus |
Publication Number: | 3401731 |
ISBN: | 978-1-109-69057-6 |