In recent years, within the broad context of mobile communication systems, a significant research has been evolved in the study of wireless ad-hoc networks. Due to the self-organizing nature of these networks, efficient delivery of data packets to the mobile nodes, where the topology is neither pre-determined nor does the network have central control, many problems arise in order to ensure a persistent communication. Packet loss in a multi-hop network is a major concern for ad-hoc distributed networks based systems. MAC layer contention is much more severe in multihop ad hoc networks as compared to wireless LANs. To mitigate this problem, we present a distributed, TDMA and slotted ALOHA protocol based communication approach for mobile robots in ad-hoc networks. Our work focuses on real time communication in a dynamic network where nodes can leave and join the network anytime. In this thesis, we propose an algorithm to establish self-sustaining communication among nodes. In our system processes become aware of their surrounding using slotted ALOHA protocol. Our system ensures self-stability by detecting lost messages and reset the system to ALOHA. Subsequently the system initiates the communication process again.
Our work shows that with combined ALOHA and TDMA protocol, a resilient and robust communication is achievable, where the packet loss is minimum. Our work also shows that self sustaining distributed communication is possible with minimum transitions to the different communication states, such as ALOHA to TDMA. This thesis demonstrates a successful communication process among mobile robotic nodes using our proposed algorithm. In this thesis, we also define the safety, liveness, and fairness properties using linear time logic (LTL) to verify the correctness of the proposed algorithm. We have defined these properties for our algorithm. We then verify the system for these properties under error prone conditions such as message loss, along with this we also make sure that our algorithm follows a fair approach of resource allocation and never end in an undesirable state. We have modeled our communication algorithm using SPIN model checker. SPIN is based on PROMELA language and provides an extensive user interface to define the model and verify the properties using Formal Methods of Verification.
|Advisor:||Ponce, Oscar Morales|
|Commitee:||Ebert, Todd, Englert, Burkhard|
|School:||California State University, Long Beach|
|Department:||Computer Engineering and Computer Science|
|School Location:||United States -- California|
|Source:||MAI 58/01M(E), Masters Abstracts International|
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