TA的每日心情 | 奋斗 2020-9-2 15:06 |
---|
签到天数: 2 天 [LV.1]初来乍到
|
EDA365欢迎您登录!
您需要 登录 才可以下载或查看,没有帐号?注册
x
摘 要: VANET网络中信息的发送和接收具有随机性和不确定性,IEEE80211p广播协议无法适应 VANET网 络拓扑动态变化,于是研究者们根据不同环境中的具体应用需求提出了各种 VANET广播协议,如何对新提出的协议 的性能以及可靠性进行分析与验证是一个关键性问题.自动化的定量验证技术能够针对系统需要满足的多个性质进 行分析,并给出满足需求的最大或者最小概率.然而研究人员在进行定量验证过程中使用的 PTCL、rPATL等逻辑语言 都不能够明确描述用户的策略是什么,因此本文提出基于概率策略逻辑的模型定量验证方法.该方法首先对系统中的 多个角色使用概率时间接口自动机对其行为建模,然后使用概率策略逻辑语言对系统需要满足的性质进行描述,最后 基于定量验证算法自动给出系统相关性质的分析结论.本文将该方法应用到 VANET信息广播协议性能分析上,能够 针对外界环境的变化选择合理的策略,从而分析出不同环境下信息广播发送成功的最大概率.
* N- P, z2 t& d9 Z# k3 u
3 o5 H3 v# b) D5 Y( u6 x
0 b! p( I( ^: |0 C }' x% q. U) S2 S. _( o) I' v& V
关键词: VANET;定量验证;基于角色的概率系统;概率策略逻辑
3 \1 V6 q$ D: W& B- ]' y, R; j: r4 g2 U, h" E7 X- Z, i' c; e
1 E2 ~5 g4 o3 O
: p+ q" e \/ X; S
附件下载:
$ f% L, V! c e9 x |
|