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.
李树秋, 刘淑芬, 王晓燕, 徐伟峰, 陆闯. 基于概率策略逻辑的VANET信息广播模型定量验证方法研究[J]. 电子学报, 2015, 43(8): 1610-1615.
LI Shu-qiu, LIU Shu-fen, WANG Xiao-yan, XU Wei-feng, LU Chuang. Quantitative Study of VANET Information Broadcasting Protocol Verification Based on Probabilistic Strategy Logic. Chinese Journal of Electronics, 2015, 43(8): 1610-1615.
[1] Zhou Lianke.Research on traffic flow density based broadcasting technologies in VANETS[D].Harbin Institute of Technology,2011.
[2] Biswas S,Tatchikou R,Dion F.Vehicle-to-vehicle wireless communication protocols for enhancing highway traffic safety[J].IEEE Communications Magazine,2006,44(1):74-82.
[3] Sproston J.Discrete-time verification and control for probabilistic rectangular hybrid automata[A].Proc 8th Int Conf Quantitative Evaluation of SysTems (QEST'11)[C].Aachen,Germany,2011,79-88.
[4] Chatterjee,K.Markov decision processes with multiple long-run average objectives[A].Proc 27th Int Conf on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07)[C].Springer,2007,473-484.
[5] Kwiatkowska M,Norman G,Segala R,Sproston J.Verifying quantitative properties of continuous probabilistic timed automata[A].Proc 11th Int Conf of Concurrency Theory(CONCUR 2000)[C].PA,USA,Springer,2000,123-137.
[6] 刘志锋,孙博,周从华.概率实时时态认知逻辑模型检测中抽象技术的研究[J].电子学报,2013,41(7):1343-1351. Liu Zhi-feng,Sun Bo,Zhou Cong-hua.Abstuaction in model checking probabilistic real-time temporal logic of knowledge[J].Acta Electronica Sinica,2013,41(7):1343-1351.(in Chinese)
[8] Norman G,Parker D,Sproston J.Model checking for probabilistic timed automata[J].Formal Methods in System Design,2013,43(2):164-190.
[9] Taolue Chen,Jian Lu.Probabilistic alternating-time temporal logic and model checking algorithm[A].Proc 4th Int Conf on Fuzzy Systems and Knowledge Discovery( FSKD 2007)[C].Haikou:IEEE,2007.35-39.
[10] Kwiatkowska M,Norman G,Parker D.PRISM 4.0:Verification of Probabilistic Real-time Systems[A].Proc 23rd Int Conf on Computer Aided Verification (CAV'11)[C].UT, USA:Springer,2011.585-591.
[11] 刘鸿飞.VANET信息广播模型与优化方法研究[D].重庆大学,2009.
2015, Vol. 43 
