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

• 作者: 刘淑芬 徐伟峰 李树秋 王晓燕 陆闯
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: VANET 定量验证 基于角色的概率系统 概率策略逻辑
• 年，卷（期）: 2015,（8）
• 所属期刊栏目: 学术论文
• 页码范围: 1610-1615
• 页数: 6页
• 分类号: TP311
• 字数: 5977字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2015.08.021

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘淑芬	吉林大学计算机科学与技术学院	96	764	14.0	21.0
2	王晓燕	吉林大学计算机科学与技术学院	47	511	13.0	22.0
3	李树秋	吉林大学计算机科学与技术学院	19	74	5.0	8.0
4	陆闯	吉林大学计算机科学与技术学院	2	3	1.0	1.0
5	徐伟峰	吉林大学计算机科学与技术学院	1	2	1.0	1.0