Resilient TDMA-based Communication Algorithm for Dynamic Ad-hoc Networks and Formal Verification

摘要

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.