CFP last date
20 December 2024
Call for Paper
January Edition
IJCA solicits high quality original research papers for the upcoming January edition of the journal. The last date of research paper submission is 20 December 2024

Submit your paper
Know more
The week's pick
Responsive image
Improved Shuffled Frog Leaping Algorithm with Self-Adaptive Shuffling for Fuzzy Logic PD+G Controller Optimization in Robotic Manipulators

Duc Hoang Nguyen
Random Articles
Reseach Article

Formal Development of Path Discovery in AODV Routing Protocol using Event-B

by Arun Kumar Singh, Divakar Yadav, Vinod Kumar Singh
journal cover thumbnail

International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 124 - Number 5
Year of Publication: 2015
Authors: Arun Kumar Singh, Divakar Yadav, Vinod Kumar Singh
10.5120/ijca2015905481

Arun Kumar Singh, Divakar Yadav, Vinod Kumar Singh . Formal Development of Path Discovery in AODV Routing Protocol using Event-B. International Journal of Computer Applications. 124, 5 ( August 2015), 24-30. DOI=10.5120/ijca2015905481

@article{ 10.5120/ijca2015905481,
author = { Arun Kumar Singh, Divakar Yadav, Vinod Kumar Singh },
title = { Formal Development of Path Discovery in AODV Routing Protocol using Event-B },
journal = { International Journal of Computer Applications },
issue_date = { August 2015 },
volume = { 124 },
number = { 5 },
month = { August },
year = { 2015 },
issn = { 0975-8887 },
pages = { 24-30 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume124/number5/22100-2015905481/ },
doi = { 10.5120/ijca2015905481 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T23:13:35.369619+05:30
%A Arun Kumar Singh
%A Divakar Yadav
%A Vinod Kumar Singh
%T Formal Development of Path Discovery in AODV Routing Protocol using Event-B
%J International Journal of Computer Applications
%@ 0975-8887
%V 124
%N 5
%P 24-30
%D 2015
%I Foundation of Computer Science (FCS), NY, USA
Abstract

An ad hoc network is collection of mobile nodes that do not have any fixed topology. In such a network, nodes are likely to join or leave the network in an arbitrary manner. Joining of any nodes is announced by itself to other neighboring nodes and nodes already present in the network learns about joining of the new node by this announcement. In such a scenario, discovery of path from one node to other node is an important task for the routing protocols used for the purpose. Adhoc on demand vector (AODV) is one routing protocol used in MANET environment. Being a reactive protocol, path discovery process in AODV is initiated by sender node when there is no routing information for an intended destination. In this paper, we present a formal model for path discovery process of the AODV protocol using Event-B. The model have been developed and checked using the RODIN tool which provides an integrated framework for development of Event-B models. Event-B technique uses a notion of refinement to specify the mathematical models of distributed systems in an incremental manner. The specifications of the system have been checked for consistency and satisfy the behavioural properties of the system expressed as invariants. All the proof obligations were discharged automatically by the RODIN tool.

References
  1. Shree Murthy, J.J. Garcia-Luna-Aveces, Distributed Bellman-Ford routing protocol (DBF), a routing protocol for packet radio networks, In Proc. ACM International Conference on Mobile Computing and Networking, pp. 86-95, Nov, 1995.
  2. M. S. Corson and A. Ephremides, A distributed routing algorithm for mobile wireless networks, In ACM Journal of Wireless Networks, vol. 1, no. 1, pp. 61-81, 1995.
  3. S. Murthy and J.J. Garcia-Luna-Aceves, An Efficient Routing Protocol for Wireless Networks, In ACM Mobile Networks and App. J., Special Issue on Routing in Mobile Communication Networks, pp. 183-97 Oct 1996.
  4. C. Perkins and P. Bhagwat, Highly dynamic destination-sequenced distance- vector routing (DSDV) for mobile computers, In ACM SIGCOMM’94 Conference on Communications Architectures, Protocols and Applications, London, UK,pp. 234-244.Aug 1994.
  5. E. Ayanoglu, S. Paul, T. F. LaPorta, K. K. Sabnani. and R. D. Gitlin. AIRMAIL: A link-layer protocol for wireless networks. In Wireless Networks, 1(1) pp. 47-60,Feb 1995.
  6. T.Chen and M. Gerla, Global State Routing: A new routing scheme for ad- hoc wireless networks, In Proc. of IEEE International Conference on Computers and Communications (ICC ‘98),Atlanta,GA,June 1998.
  7. Mario Gerla, Guangyu Pei, Xiaoyan Hong, Tsu-Wei Chen, Fisheye State Routing Protocol (FSR) for Ad Hoc Networks , Internet Draft, draft-ietfm anet-fsr-00.txt, work in progress, June 2001.
  8. J. Garcia-Luna, M. Spohn. Source Tree Adaptive Routing Internet Draft, draft-ietf-manet-star-00.txt, work in progress, October 1999.
  9. T. Clausen, P. Jacquet, P. Muhlethaler, A. Laouiti, A. Qayyum, and L. Viennot, Optimized link state routing protocol, In IEEE INMIC’Ol, Lahore, Pakistan, Dec 2001.
  10. Mario Gerla, Xiaoyan Hong, Li Ma, Guangya Pei, Landmark routing protocol (LANM4R), Internet Draft, draft-ietf-manet-lanmar-0 I .txt, work in progress, June 2001.
  11. C. E. Perkins and E. M. Royer, Ad-hoc On-Demand Distance Vector Routing, In Proc. of the 2nd IEEE Workshop on Mobile Computing Systems and Applications, pp. 90-100. New Orleans, LA, Feb 1999.
  12. Y.C. Hu and D. B. Johnson, Caching -strategies in on-demand routing protocols for wireless ad hoc network, In Proc. 6th Annual ACM/IEEE International Conf. on Mobile Computing and Networking (ACMMobiCom ‘00), pp 231-242, Aug 2000.
  13. M.S. Ccorson and A. Ephremides, Lightweight mobile routing protocol (LMR) ,A distributed routing algorithm for mobile wireless networks, Wireless Networks 1 (1995).
  14. D. B. Johnson, D. A. Maltz, and J. Broch, DSR: The dynamic source routing protocol for multihop wireless ad hoc netivorks, In Ad Hoc Networking. Addison-Wesley, 2001, ch. 5, pp. 139-172.
  15. Josh Broch, David Johnson, and David Maltz, The dynamic source routing protocol for mobile ad hoc networks, http://www.ietf.orglintemet-drafts/ draft-ietfm anet-dsr-03.txt, Oct 1999. IETF Internet Draft
  16. ‘Joa-Ng and I.-T. Lu, A Peer-to-Peer zone-based two-level link state routing for mobile Ad hoc Networks, In IEEE Journal on Selected Areas in Communications, Special Issue on ad-hoc networks, Aug1999, pp.1415-25.
  17. C. E. Perkins and E. M. Royer, Ad-hoc On-Demand Distance Vector Routing, In Proc. of the 2nd IEEE Workshop on Mobile Computing Systems and Applications, pp. 90-100. New Orleans, LA, Feb 1999.
  18. Christel Baier and Joost-Pieter Katoen: Principles of Model Checking. The MIT Press, 2008.
  19. Gerhard J. Holzmann: The Spin Model Checker: Primer and Reference Manual. Addison–Wesley, 2003.
  20. Marco Devillers, David Griffioen, Judi Romijn, and Frits Vaandrager: Verification of a leader election protocol: Formal methods applied to ieee 1394. Form. Methods Syst. Des.,16(3):307–320, 2000.
  21. Abrial, J.R., J.R., Cansell, D.,M´ery, D.:A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol. Formal Asp. Comput. 14(3), 215–227, 2003.
  22. A Udaya Shankar and Simon S Lam: A stepwise refinement heuristic for protocol construction.ACM Transactions on Programming Languages and Systems, 14(3):417–461,1992.
  23. Dominique M´ery and Neeraj Kumar Singh:Analysis of DSR Protocol in Event-B 13thInternational Symposium on Stabilization, Safety, and Security of Distributed Systems (2011)401-415.
  24. Arun Kumar Singh, Divakar Yadav and Vinod Kumar Singh , 2014. MODELING OF DSDV ROUTING PROTOCOL FOR AD HOC NETWORKS USING EVENT-B. International Journal of Computer Engineering & Technology (IJCET) Volume:5, Issue :2, Pages:108-116.
  25. Singh, A.K and Singh, V.K.: Formal Modeling of Distance Vector Routing Protocol using Event-B in Advance in Electronic and Electric Engineering ISSN 2231-1297, Volume 3,Number 1 (2013), pp. 91-98.
  26. Hoang, T.S., Kuruma, H., Basin, D.A., Abrial, J.R.: Developing Topology Discovery in Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 1–19.Springer, Heidelberg (2009).
  27. Jean-Raymond Abrial. The B-book: assigning programs to meanings. CambridgeUniversity Press, 1996.
  28. Ralph-Johan Back and Reino Kurki-Suonio. Decentralization of process nets with centralized control. Distributed Computing, 3(2):73–87, 1989.
  29. Abrial, J.R.:Modeling in Event-B: System and Software Design. Cambridge University Press, 2010.
  30. Abrial, J.R.: Extending B without Changing it (for developing distributed systems). Proc. of the 1st Conf. on the B method, H. Habrias (editor), France, pages 169–190, 1996.
Index Terms

Computer Science
Information Sciences

Keywords

MANET AODV Formal Method Event-B.

Powered by PhDFocusTM