Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Implementation of SPIN Model C...

Implementation of SPIN Model Checker for Formal Verification of Distance Vector Routing Protocol

Kashif Javed, Kashif Asifa, Elena Troubitsyna, Implementation of SPIN Model Checker for Formal Verification of Distance Vector Routing Protocol. International Journal of Computer Science and Information Security 8(3), 6, 2010.

Abstract:

Distributed systems and computing requires routing protocols to meet a wide variety of requirements of a large number of users in heterogeneous networks. DVR is one of many other employed protocols for establishing communication using routes with minimum cost to different destinations from a given source. Research work presented in this paper focuses on
implementation of DVR in SPIN and provides formal verification of correctness of DVR behaviour covering all required aspects. Simulation results clearly show a proof of the established paths from each router to different destinations in a network consisting of six routers and a number of links.

Files:

Full publication in PDF-format

BibTeX entry:

@ARTICLE{jKa10a,
  title = {Implementation of SPIN Model Checker for Formal Verification of Distance Vector Routing Protocol},
  author = {Javed, Kashif and Asifa, Kashif and Troubitsyna, Elena},
  journal = {International Journal of Computer Science and Information Security},
  volume = {8},
  number = {3},
  pages = {6},
  year = {2010},
  keywords = {Formal Verification, DVR Protocol, SPIN Model Checker, Distance Vector Routing, Implementation in PROMELA},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication