Please use this identifier to cite or link to this item:
|Title:||Formal Modelling and Verification of Requirements of Adaptive Routing Protocol for Mobile Ad-Hoc Network|
Mobile Ad-Hoc Network (MANET)
Yices SMT Solver
|Abstract:||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. � 2017 IEEE.|
|Appears in Collections:||Research Publications|
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.