基于概率模型檢測(cè)的網(wǎng)絡(luò)協(xié)議的性能與可靠性分析.pdf

1、概率模型檢測(cè)是一種形式化的驗(yàn)證方法，它首先將目標(biāo)系統(tǒng)建模成一個(gè)概率模型，并用概率時(shí)序邏輯刻畫要驗(yàn)證的屬性，然后判定模型是否滿足此屬性，或是求解屬性的值。相對(duì)于實(shí)驗(yàn)和仿真，概率模型檢測(cè)系統(tǒng)地探索整個(gè)狀態(tài)空間，因此允許對(duì)系統(tǒng)所有可能的行為進(jìn)行推理，提高了屬性驗(yàn)證的精確性和全面性。目前概率模型檢測(cè)已經(jīng)在分析系統(tǒng)的可靠性，安全性等性能方面獲得了廣泛的應(yīng)用。本文利用概率模型檢測(cè)技術(shù)對(duì)面向海量數(shù)據(jù)可靠快速傳輸?shù)目焖侔踩珔f(xié)議(FASP)和應(yīng)用于車載網(wǎng)

2、絡(luò)通信的IEEE802.11P中的介質(zhì)訪問(wèn)控制(MAC)協(xié)議的性能與可靠性進(jìn)行了詳細(xì)的分析，所有的工作均是在模型檢測(cè)工具PRISM上面完成，主要內(nèi)容有:
　　 1.對(duì)于FASP協(xié)議，根據(jù)傳輸特性，特別是負(fù)反饋機(jī)制及單一數(shù)據(jù)流的連續(xù)性，將其建模為一個(gè)連續(xù)時(shí)間馬爾可夫鏈(CTMC)模型。然后對(duì)FASP協(xié)議最重要的兩個(gè)屬性—可靠性和快速性—進(jìn)行了驗(yàn)證分析。從概率模型角度出發(fā)，我們將可靠性描述成:發(fā)送端總是能完成數(shù)據(jù)的發(fā)送，并且接收端最

3、終將成功接收，這一事件的概率是否總是為1。驗(yàn)證結(jié)果表明，無(wú)論丟失率如何改變，此概率一直保持為1，這充分說(shuō)明FASP有很好的可靠性能。在驗(yàn)證快速性時(shí)，分析了所要發(fā)送的數(shù)據(jù)量，信道傳輸速度及信道的數(shù)據(jù)丟失率三個(gè)參數(shù)的不同取值對(duì)傳輸時(shí)間的影響，我們發(fā)現(xiàn)無(wú)論網(wǎng)絡(luò)配置如何，F(xiàn)ASP完成1G大小的文件傳輸大概僅需10秒，說(shuō)明FASP傳輸數(shù)據(jù)的速度非常快。最后，利用吞吐量計(jì)算公式獲得了FASP的吞吐量，將其與TCP吞吐量進(jìn)行對(duì)比，結(jié)果表明，F(xiàn)ASP吞

4、吐量能完全獨(dú)立于網(wǎng)絡(luò)延遲并且對(duì)極端的包丟失率具備魯棒性。
　　 2.IEEE802.11P的MAC協(xié)議支持密集時(shí)間，概率選擇和非確定性，所以我們選擇能同時(shí)支持這三種特性的概率時(shí)間自動(dòng)機(jī)(PTA)對(duì)MAC建模。然后對(duì)802.11P的兩種不同類型的性能指標(biāo):概率可達(dá)性和期望可達(dá)性進(jìn)行了驗(yàn)證分析。概率可達(dá)性首先驗(yàn)證了802.11P總是能完成數(shù)據(jù)的發(fā)送，其次計(jì)算了任意站的退避計(jì)數(shù)器達(dá)到最大退避數(shù)的概率，這是退避過(guò)程中的最壞情況的概率，此

5、概率隨著最大退避數(shù)的增加急劇下降，并且802.11P的概率比802.11標(biāo)準(zhǔn)要小得多，這表示802.11P因發(fā)生沖突而進(jìn)入等待的情況會(huì)明顯減少，在高速行駛的情況下也能及時(shí)發(fā)送數(shù)據(jù)。期望可達(dá)性分析了，802.11P完成數(shù)據(jù)發(fā)送前發(fā)生沖突的期望次數(shù)最多的情況，以及完成數(shù)據(jù)傳輸所需要的最長(zhǎng)的時(shí)間。兩個(gè)站都正確發(fā)送數(shù)據(jù)前，發(fā)生沖突的最大期望次數(shù)的結(jié)果發(fā)明，802.11P發(fā)生沖突的情況比802.11標(biāo)準(zhǔn)稍微緩和，穩(wěn)定性也更好。完成相同數(shù)據(jù)大小的發(fā)