JCS Cover
Frequency: Monthly
ISSN: 1549-3636 (Print)
ISSN: 1552-6607 (Online)
Research Article Open Access

FORMAL VERIFICATION OF SAFETY MESSAGE DISSEMINATION PROTOCOL FOR VANETS

M. A. Berlin1 and Sheila Anand1
  • 1 Anna University, India

Abstract

This paper presents a formal verification of a safety message dissemination protocol used in vehicular ad-hoc networks. It is proposed to use Road Side Units to broadcast road hazard information to vehicles travelling on highways. Quick dissemination of road hazard information, like road blocks, slippery roads and other obstacles can help to prevent road accidents and improve passenger safety. Formal verification is a mathematical approach that helps developers to validate the protocol and correct design errors. The well known model checker, SPIN has been used to model the possible behavior of the protocol and provide formal verification of the correctness of the protocol.

Journal of Computer Science
Volume 9 No. 8, 2013, 1069-1078

DOI: https://doi.org/10.3844/jcssp.2013.1069.1078

Submitted On: 22 May 2013 Published On: 9 July 2013

How to Cite: Berlin, M. A. & Anand, S. (2013). FORMAL VERIFICATION OF SAFETY MESSAGE DISSEMINATION PROTOCOL FOR VANETS. Journal of Computer Science, 9(8), 1069-1078. https://doi.org/10.3844/jcssp.2013.1069.1078

Open AccessCopyright: © 2013 M. A. Berlin and Sheila Anand. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.

  • 3,369 Views
  • 3,539 Downloads
  • 4 Citations

Download

Keywords

  • Safety Message Dissemination Protocol
  • Road Side Units
  • Road Hazard
  • Highways
  • Formal Verification
  • SPIN Model Checker