论文部分内容阅读
概率模型检测是一种形式化的验证方法，它首先将目标系统建模成一个概率模型，并用概率时序逻辑刻画要验证的属性，然后判定模型是否满足此属性，或是求解属性的值。相对于实验和仿真，概率模型检测系统地探索整个状态空间，因此允许对系统所有可能的行为进行推理，提高了属性验证的精确性和全面性。目前概率模型检测已经在分析系统的可靠性，安全性等性能方面获得了广泛的应用。本文利用概率模型检测技术对面向海量数据可靠快速传输的快速安全协议(FASP)和应用于车载网络通信的IEEE802.11P中的介质访问控制(MAC)协议的性能与可靠性进行了详细的分析，所有的工作均是在模型检测工具PRISM上面完成，主要内容有:
1.对于FASP协议，根据传输特性，特别是负反馈机制及单一数据流的连续性，将其建模为一个连续时间马尔可夫链(CTMC)模型。然后对FASP协议最重要的两个属性—可靠性和快速性—进行了验证分析。从概率模型角度出发，我们将可靠性描述成:发送端总是能完成数据的发送，并且接收端最终将成功接收，这一事件的概率是否总是为1。验证结果表明，无论丢失率如何改变，此概率一直保持为1，这充分说明FASP有很好的可靠性能。在验证快速性时，分析了所要发送的数据量，信道传输速度及信道的数据丢失率三个参数的不同取值对传输时间的影响，我们发现无论网络配置如何，FASP完成1G大小的文件传输大概仅需10秒，说明FASP传输数据的速度非常快。最后，利用吞吐量计算公式获得了FASP的吞吐量，将其与TCP吞吐量进行对比，结果表明，FASP吞吐量能完全独立于网络延迟并且对极端的包丢失率具备鲁棒性。
2.IEEE802.11P的MAC协议支持密集时间，概率选择和非确定性，所以我们选择能同时支持这三种特性的概率时间自动机(PTA)对MAC建模。然后对802.11P的两种不同类型的性能指标:概率可达性和期望可达性进行了验证分析。概率可达性首先验证了802.11P总是能完成数据的发送，其次计算了任意站的退避计数器达到最大退避数的概率，这是退避过程中的最坏情况的概率，此概率随着最大退避数的增加急剧下降，并且802.11P的概率比802.11标准要小得多，这表示802.11P因发生冲突而进入等待的情况会明显减少，在高速行驶的情况下也能及时发送数据。期望可达性分析了，802.11P完成数据发送前发生冲突的期望次数最多的情况，以及完成数据传输所需要的最长的时间。两个站都正确发送数据前，发生冲突的最大期望次数的结果发明，802.11P发生冲突的情况比802.11标准稍微缓和，稳定性也更好。完成相同数据大小的发送，802.11P所用的时间大约只有802.11标准的四分之一，发送数据的平均速度约为802.11标准的4倍。