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

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

作　　者：李树秋[1] 刘淑芬[1] 王晓燕[1] 徐伟峰[1] 陆闯[1] 

机构地区：[1]吉林大学计算机科学与技术学院

出　　处：《电子学报》2015年第8期1610-1615,共6页Acta Electronica Sinica

基　　金：国家自然科学基金(No.60973041)

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]