Formal Verification of Congestion Control Algorithm in VANETs

Full Text (PDF, 345KB), PP.1-7

Views: 0 Downloads: 0


Mohamad Yusof Darus 1,* Kamalrulnizam Abu Bakar 1

1. Faculty of Computer Science & Information Systems, Universiti Teknologi Malaysia (UTM), Malaysia

* Corresponding author.


Received: 6 Jul. 2012 / Revised: 12 Nov. 2012 / Accepted: 5 Jan. 2013 / Published: 8 Apr. 2013

Index Terms

VANETs, Congestion control, Event-driven safety message, Beacon messages, CCH channel


A Vehicular Ad-Hoc Networks (VANETs) is the technology that uses moving cars as nodes in a network to create a mobile network. VANETs turn every participating car into a wireless router, allowing cars of each other to connect and create a network with a wide range. VANETs are developed for enhancing the driving safety and comfort of automotive users. The VANETs can provide wide variety of service such as Intelligent Transportation System (ITS) e.g. safety applications. Many of safety applications built in VANETs are required real-time communication with high reliability. One of the main challenges is to avoid degradation of communication channels in dense traffic network. Many of studies suggested that appropriate congestion control algorithms are essential to provide efficient operation of the network. However, most of congestion control algorithms are not really applicable to event-driven safety messages. In this paper we propose congestion control algorithm as solution to prevent congestion in VANETs environment. We propose a complete validation method and analyse the performance of our congestion control algorithms for event-driven safety messages in difference congested scenarios. The effectiveness of the proposed congestion control algorithm is evaluated through the simulation using Veins simulator.

Cite This Paper

Mohamad Yusof Darus, Kamalrulnizam Abu Bakar, "Formal Verification of Congestion Control Algorithm in VANETs", International Journal of Computer Network and Information Security(IJCNIS), vol.5, no.4, pp.1-7, 2013. DOI:10.5815/ijcnis.2013.04.01


[1]Hendriks, L., Effects of Transmission Queue Size, Buffer and Scheduling Mechanisms on the IEEE 802.11p Beaconing Performance, 15th Twente Student Conference, University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science. (2011).
[2]Konur, S. and Fisher, M., Formal Analysis of a VANET Congestion Control Protocol through Probabilistic Verification, In proceeding IEEE 73rd Vehicular Technology Conference (VTC Spring), Budapest, (2011), pp. 1 – 5
[3]Li, M., Lou, W., & Zeng, K., OppCast: Opportunistic Broadcast of Warning Messages in VANETs with Unreliable Links. In Proc. IEEE 6th International Conference (MASS '09). (2009), 534 – 543
[4]Campolo, C., Cortese, A., & Molinaro, A., CRaSCH A Cooperative Scheme for Service Channel Reservation in 802.11p/WAVE Vehicular Ad Hoc Networks. In Proc. International Conference on Ultra Modern Telecommunications & Workshops. (2009), 1-8
[5]Wang, Y., Ahmed, A., Krishnamachari, B., & Psounis, K., IEEE 802.11p Performance Evaluation and Protocol Enhancement. In Proc IEEE International Conference on Vehicular Electronics and Safety Columbus. (2008), 317-322.
[6]Bilstrup, K. , Uhlemann, E., Strom, E.G. & Bilstrup, U., Evaluation of the IEEE 802.11p MAC method for Vehicle-to-Vehicle Communication. In Proc. IEEE 68th Vehicular Technology Conference.(2008), 1-5
[7]Bouassida, M.S., and Shawky, M., On The Congestion Control Within Vanet. 1st IFIP Wireless Days.(2008), 1-5.
[8]Zang, Y.P., Stibor, L., Cheng, X., Reumerman, H. J., Paruzel A., & Barroso, A., Congestion Control in Wireless Networks for Vehicular Safety Applications. In Proc. of The 8th European Wireless Conference. (2007), 7.
[9]He, J., Chen, H.C. et al., Adaptive Congestion Control for DSRC Vehicle Networks, IEEE Communications Letters. (2010), Vol. 14, No. 2.
[10]Lomuscio, A., Strulo, B. et al. (2009). Model Checking Optimisation Based Congestion Control Models. Research notes from University College London, 2009
[11]Sommer, C., Tonguz, O. and Dressler, F., Traffic Information Systems: Efficient Message Dissemination via Adaptive Beaconing. IEEE Communication Magazine.49, (2011), 173 – 179. IEEE.
[12]Tsao, S.L. and Cheng, C.M., Design and Evaluation of A Two-Tier Peer-To-Peer Traffic Information System. IEEE Communication Magazine. 49, (2011), 165 – 172. IEEE.