基于概率模型检测的网络协议的性能与可靠性分析

摘要

概率模型检测是一种形式化的验证方法，它首先将目标系统建模成一个概率模型，并用概率时序逻辑刻画要验证的属性，然后判定模型是否满足此属性，或是求解属性的值。相对于实验和仿真，概率模型检测系统地探索整个状态空间，因此允许对系统所有可能的行为进行推理，提高了属性验证的精确性和全面性。目前概率模型检测已经在分析系统的可靠性，安全性等性能方面获得了广泛的应用。本文利用概率模型检测技术对面向海量数据可靠快速传输的快速安全协议(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倍。

目录

声明

摘要

第一章 绪论

1．1 研究背景

1．1．1 快速安全协议FASP

1．1．2 IEEE 802．11P及其MAC协议

1．2 研究现状

1．2．1 快速安全协议的分析

1．2．2 IEEE 802．11P的分析

1．3 研究内容及论文组织

第二章 相关的概念和定义

2．1 基础定义

2．2 离散时间马尔可夫链

2．3 连续时间马尔可夫链

2．4 马尔可夫决策过程

2．5 概率时间自动机

2．6 PRISM

2．7 建模过程

第三章 快速安全协议建模

3．1 FASP解决方案

3．2 FASP建模

3．3 本章小节

第四章 快速安全协议的分析

4．1 FASP模型统计

4．2 性能属性分析

4．2．1 FASP的可靠性分析

4．2．2 FASP的快速性分析

4．2．3 吞吐量

4．3 本章小节

第五章 IEEE 802．11P的MAC协议建模

5．1 IEEE802．11P的MAC协议的工作特性

5．2 MAC协议的PTA模型

5．3 本章小节

第六章 IEEE 802．11P的分析

6．1 802．11P模型的静态数据分析

6．2 802．11P模型的验证分析

6．2．1 802．11P模型的概率可达性

6．2．2 802．11P模型的期望可达性

6．3 本章小结

第七章 结论与展望

7．1 结论

7．2 展望

参考文献

致谢

攻读硕士学位期间发表的论文