The transmission and reception of information in VANET has the property of randomness and uncertainty.Due to the inadaptability of IEEE 802.11p broadcast protocol to the dynamic changes of VANET topology

researchers proposed VANET broadcasting protocol on the basis of specific application requirements.Therefore

the key is how to analyze and verify the performance and reliability of the updated protocol.Automated quantitative verification can analyze the properties of the system requirements and provide the maximum or minimum probability.However

PTCL and rPATL are found not to precisely represent the strategies of the users in the quantitative verification process delivered by researchers.For this purpose

the method namely

Quantitative Model Verification based on Probabilistic Strategy Logic' is proposed.Firstly

interval probabilistic timed interface automata are applied to model the behavior for each role in the system

then probabilistic strategy logic is adopted to describe the properties to meet the requirements and quantitative validation algorithm is given.Finally

the method is applied to the VANET information broadcast protocol.The proposed model can select a reasonable strategy revolving the external changes and analyze the maximum probability for a successful transmission of information broadcast.