Quantitative model verification in VANET based on interval probabilistic timed automata

VANET is developed as a standard means of communication among moving vehicles. In VANET a vehicle needs to periodically exchange message with its neighbors so that they are aware of any changes to the surrounding vehicles. But the emergency message is event driven, the occurrence of it is unpredictable. So it is important to verify that emergency message can transmit reliably on rapidly changing vehicular channels. In recent years, an automated verification technique for probabilistic models has been developed. In this paper, we propose a formal method to quantitatively verify the probability of message transmission under variant different conditions.