• Aug 09, 2018 News![CFP] The annual meeting of IJFCC Editorial Board, ICCTD 2019, will be held in Prague, Czech Republic during March 2-4, 2019.   [Click]
  • Aug 09, 2018 News!IJFCC Vol. 6, No. 1-No. 3 has been indexed by EI (Inspec).   [Click]
  • Oct 26, 2018 News!The papers published in Vol.6, No.3-No.4 have all received dois from Crossref.
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. Cherry L. Chan
    • Abstracting/ Indexing: Google Scholar,  Crossref, Electronic Journals LibraryEI (INSPEC, IET), etc.
    • E-mail:  ijfcc@ejournal.net 
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.


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-2018. International Journal of Future Computer and Communication. All rights reserved.
E-mail: ijfcc@ejournal.net