Visible to the public Formal Modelling and Verification of Requirements of Adaptive Routing Protocol for Mobile Ad-Hoc Network

TitleFormal Modelling and Verification of Requirements of Adaptive Routing Protocol for Mobile Ad-Hoc Network
Publication TypeConference Paper
Year of Publication2017
AuthorsTripathy, B. K., Sudhir, A., Bera, P., Rahman, M. A.
Conference Name2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC)
KeywordsAdaptation models, adaptive routing protocol, composability, formal modelling, formal verification, MANET, mobile ad hoc networks, mobile ad-hoc network, Mobile Ad-Hoc Network (MANET), Mobile communication, mobile nodes, Network topology, pubcrawl, QoS constraints, quality of service, quality-of-service constraints, requirement constraints, requirement models, resilience, Resiliency, Routing, routing functions, Routing Protocol, Routing protocols, Scalability, secure routing protocol, security, SMT-LIB, SMT-LIB language, Trust Routing, Yices SMT Solver

A group of mobile nodes with limited capabilities sparsed in different clusters forms the backbone of Mobile Ad-Hoc Networks (MANET). In such situations, the requirements (mobility, performance, security, trust and timing constraints) vary with change in context, time, and geographic location of deployment. This leads to various performance and security challenges which necessitates a trade-off between them on the application of routing protocols in a specific context. The focus of our research is towards developing an adaptive and secure routing protocol for Mobile Ad-Hoc Networks, which dynamically configures the routing functions using varying contextual features with secure and real-time processing of traffic. In this paper, we propose a formal framework for modelling and verification of requirement constraints to be used in designing adaptive routing protocols for MANET. We formally represent the network topology, behaviour, and functionalities of the network in SMT-LIB language. In addition, our framework verifies various functional, security, and Quality-of-Service (QoS) constraints. The verification engine is built using the Yices SMT Solver. The efficacy of the proposed requirement models is demonstrated with experimental results.

Citation Keytripathy_formal_2017