Dissertation/Thesis Abstract

Modeling and verification techniques for ad hoc network protocols
by Singh, Anu, Ph.D., State University of New York at Stony Brook, 2009, 130; 3401731
Abstract (Summary)

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.

Indexing (document details)
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
Subjects: Computer science
Keywords: Ad hoc networks, Formal verification, MANETs, Omega calculus
Publication Number: 3401731
ISBN: 978-1-109-69057-6
Copyright © 2021 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy