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