VERIFICATION OF CONGESTION CONTROL PROTOCOL IN VANETs USING FORMAL METHOD

Congestion control protocols developed in order to resolve the issue of congestion in VANETs must ensure reliable communication of safety-related messages. In this work we focused on formally verifying congestion control protocol in VANETs using model checking technique. The protocol was formally modeled using a network of timed automata. The model was verified against reachability, safety and liveness properties to analyze the reliability and functional aspects of the protocol. A model checking tool UPPAAL was used for formally modelling, simulating and verifying the protocol.