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.|
|School:||State University of New York at Stony Brook|
|School Location:||United States -- New York|
|Source:||DAI-B 71/04, Dissertation Abstracts International|
|Keywords:||Ad hoc networks, Formal verification, MANETs, Omega calculus|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be