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.
