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

• 学术论文 • 上一篇    下一篇

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

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

  1. 吉林大学计算机科学与技术学院, 吉林长春 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   

  1. 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

摘要:

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

中图分类号: