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

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

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

3、終將成功接收，這一事件的概率是否總是為1。驗證結(jié)果表明，無論丟失率如何改變，此概率一直保持為1，這充分說明FASP有很好的可靠性能。在驗證快速性時，分析了所要發(fā)送的數(shù)據(jù)量，信道傳輸速度及信道的數(shù)據(jù)丟失率三個參數(shù)的不同取值對傳輸時間的影響，我們發(fā)現(xiàn)無論網(wǎng)絡(luò)配置如何，F(xiàn)ASP完成1G大小的文件傳輸大概僅需10秒，說明FASP傳輸數(shù)據(jù)的速度非?？臁Ｗ詈螅猛掏铝坑嬎愎将@得了FASP的吞吐量，將其與TCP吞吐量進(jìn)行對比，結(jié)果表明，F(xiàn)ASP吞

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

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