• Jan 05, 2017 News![CFP] 2017 the annual meeting of IJFCC Editorial Board, ICCTD 2017, will be held in Paris, France during March 20-22, 2017.   [Click]
  • Mar 24, 2016 News! IJFCC Vol. 4, No. 4 has been indexed by EI (Inspec).   [Click]
  • Jun 28, 2017 News!Vol.6, No.3 has been published with online version.   [Click]
General Information
    • ISSN: 2010-3751
    • Frequency: Bimonthly (2012-2016); Quarterly (Since 2017)
    • DOI: 10.18178/IJFCC
    • Editor-in-Chief: Prof. Mohamed Othman
    • Executive Editor: Ms. Nancy Y. Liu
    • Abstracting/ Indexing: Google Scholar, Engineering & Technology Digital Library, and Crossref, DOAJ, Electronic Journals LibraryEI (INSPEC, IET).
    • E-mail:  ijfcc@ejournal.net 
Editor-in-chief
Prof. Mohamed Othman
Department of Communication Technology and Network Universiti Putra Malaysia, Malaysia
It is my honor to be the editor-in-chief of IJFCC. The journal publishes good papers in the field of future computer and communication. Hopefully, IJFCC will become a recognized journal among the readers in the filed of future computer and communication.
IJFCC 2014Vol.3(5): 325-330 ISSN: 2010-3751
DOI: 10.7763/IJFCC.2014.V3.320

Formal Analysis of a Ranked Neighbour MANET Protocol Suite

Shamim H. Ripon, Syed Fahin Ahmed, Afroza Yasmin, Yeaminar Rashid, and K. M. Imtiaz-Ud-Din
Abstract—Formal verification plays an important role in development and application of safety critical systems. Formalized verification techniques to analyze the security and the safety properties of communication protocols increase and confirm the protocol confidence the advancement of mobile and wireless communication technologies in recent years introduced various adaptive protocols to adapt the need for secured communications. Security is a crucial success factor for any communication protocols, especially in mobile environment due to its ad hoc behavior. SPIN is a powerful model checker that verifies the correctness of distributed communication models in a rigorous and automated fashion. This paper presents a SPIN based formal verification approach of a security adaptive protocol suite. The protocol suite includes a neighbor discovery mechanism and routing protocol. The protocol suite is encoded into SPIN and is exhaustively checked for various temporal properties ensuring the applicability of the protocol suite in real-life applications.

Index Terms—Ranked neighbor, SPIN, model checking, loop freedom.

S. H. Ripon is with the East West University, Dhaka, Bangladesh (e-mail: dshr@ewubd.edu).
S. F. Ahmed, A. Yasmin, Y. Rashid, and K.M. Imtiaz-Ud-Din are with the Department of Computer Science and Engineering, East West University, Dhaka, Bangladesh.

[PDF]

Cite: Shamim H. Ripon, Syed Fahin Ahmed, AfrozaYasmin, Yeaminar Rashid, and K. M. Imtiaz-Ud-Din, "Formal Analysis of a Ranked Neighbour MANET Protocol Suite," International Journal of Future Computer and Communication vol. 3, no. 5, pp. 325-330, 2014.

Copyright © 2008-2016. International Journal of Future Computer and Communication. All rights reserved.
E-mail: ijfcc@ejournal.net