TY  - JOUR
AU  - Berlin, M. A. 
AU  - Anand, Sheila 
PY  - 2013
TI  - FORMAL VERIFICATION OF SAFETY MESSAGE DISSEMINATION PROTOCOL FOR VANETS
JF  - Journal of Computer Science
VL  - 9
IS  - 8
DO  - 10.3844/jcssp.2013.1069.1078
UR  - https://thescipub.com/abstract/jcssp.2013.1069.1078
AB  - 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.