基于概率策略逻辑的VANET信息广播模型定量验证方法研究

doi:10.3969/j.issn.0372-2112.2015.08.021

电子学报 ›› 2015, Vol. 43 ›› Issue (8): 1610-1615.DOI: 10.3969/j.issn.0372-2112.2015.08.021

基于概率策略逻辑的VANET信息广播模型定量验证方法研究

李树秋, 刘淑芬, 王晓燕, 徐伟峰, 陆闯

吉林大学计算机科学与技术学院, 吉林长春 130012

收稿日期:2014-05-04 修回日期:2014-12-28 出版日期:2015-08-25
- 通讯作者:
- 王晓燕
- 作者简介:
- 李树秋 男,1966年出生,黑龙省江尚志县人,吉林大学计算机学院副教授,工学硕士.研究方向为计算机协同、计算机应用. E-mail:shuqiu@jlu.edu.cn 刘淑芬 女,1950年出生,教授,博士生导师.研究方向为计算机支持协同工作、软件体系结构、基于模型驱动的软件编程方法. E-mail:liusf@jlu.edu.cn
- 基金资助:
- 国家自然科学基金 (No.60973041)

Quantitative Study of VANET Information Broadcasting Protocol Verification Based on Probabilistic Strategy Logic

LI Shu-qiu, LIU Shu-fen, WANG Xiao-yan, XU Wei-feng, LU Chuang

College of Computer Science and Technology, Jilin University, Changchun, Jilin 130012, China

Received:2014-05-04 Revised:2014-12-28 Online:2015-08-25 Published:2015-08-25

摘要/Abstract

摘要：

VANET网络中信息的发送和接收具有随机性和不确定性,IEEE 802.11p广播协议无法适应VANET网络拓扑动态变化,于是研究者们根据不同环境中的具体应用需求提出了各种VANET广播协议,如何对新提出的协议的性能以及可靠性进行分析与验证是一个关键性问题.自动化的定量验证技术能够针对系统需要满足的多个性质进行分析,并给出满足需求的最大或者最小概率.然而研究人员在进行定量验证过程中使用的PTCL、rPATL等逻辑语言都不能够明确描述用户的策略是什么,因此本文提出基于概率策略逻辑的模型定量验证方法.该方法首先对系统中的多个角色使用概率时间接口自动机对其行为建模,然后使用概率策略逻辑语言对系统需要满足的性质进行描述,最后基于定量验证算法自动给出系统相关性质的分析结论.本文将该方法应用到VANET信息广播协议性能分析上,能够针对外界环境的变化选择合理的策略,从而分析出不同环境下信息广播发送成功的最大概率.

关键词: VANET, 定量验证, 基于角色的概率系统, 概率策略逻辑

Abstract:

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.

Key words: vchicular ad hoc networks(VANET), quantitative verification, probabilistic system based on roles, probabilistic strategy logic

中图分类号:

TP311

李树秋, 刘淑芬, 王晓燕, 徐伟峰, 陆闯. 基于概率策略逻辑的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[J]. Acta Electronica Sinica, 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.

基于概率策略逻辑的VANET信息广播模型定量验证方法研究

Quantitative Study of VANET Information Broadcasting Protocol Verification Based on Probabilistic Strategy Logic

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 1

编辑推荐

Metrics