陳立斌, 文 英

(1. 湖南理工學(xué)院 計(jì)算機(jī)學(xué)院, 湖南 岳陽(yáng) 414006; 中國(guó)移動(dòng)集團(tuán)廣西有限公司 南寧分公司, 南寧 530028)

Ad Hoc網(wǎng)絡(luò)中有限重傳協(xié)議的建模與分析

陳立斌1, 文 英2

(1. 湖南理工學(xué)院 計(jì)算機(jī)學(xué)院, 湖南 岳陽(yáng) 414006; 中國(guó)移動(dòng)集團(tuán)廣西有限公司 南寧分公司, 南寧 530028)

在節(jié)點(diǎn)不斷移動(dòng)、拓?fù)鋭?dòng)態(tài)變化、帶寬受到限制的Ad Hoc網(wǎng)絡(luò)中, 節(jié)點(diǎn)間的通信會(huì)受到收發(fā)節(jié)點(diǎn)間相鄰概率、信道質(zhì)量等因素的影響. 本文應(yīng)用概率模型檢測(cè)技術(shù), 基于有限狀態(tài)機(jī)和馬爾可夫決策過(guò)程, 對(duì)Ad Hoc網(wǎng)絡(luò)環(huán)境中的有限重傳協(xié)議進(jìn)行建模, 并使用PRISM工具量化分析了節(jié)點(diǎn)間信道質(zhì)量、文件的分組數(shù)和重傳的最大次數(shù)對(duì)網(wǎng)絡(luò)通信的影響, 驗(yàn)證了協(xié)議相關(guān)性質(zhì), 分析結(jié)果有助于根據(jù)網(wǎng)絡(luò)實(shí)際情況設(shè)置協(xié)議各參數(shù), 從而提高網(wǎng)絡(luò)性能.

有限重傳協(xié)議; Ad Hoc網(wǎng)絡(luò); 概率模型檢測(cè); PRISM

Abstract:In Ad Hoc network, mobile node with limited bandwidth moves frequently and topology changes dynamically. The communication between nodes is dynamically affected by many factors, such as the neighbor probability, channel quality and so on. Based on Probabilistic Model Checking, the Bounded Retransmission Protocol (BRP) in Ad Hoc Network is modeled. Then the influence of channel quality, the number of data frames and the maximum number of retransmission on the communication are analyzed with Probabilistic Model Checking tool-PRISM. The analysis results are helpful to adjust various parameters of protocol according to the different situation in order to improve the performance of the network.

Key words:bounded retransmission protocol; Ad Hoc network; probabilistic model checking; PRISM

引言

有限重傳協(xié)議[1,2](Bounded Retransmission Protocol, BRP)是一種用于不可靠通信線路上傳送大型數(shù)據(jù)包的數(shù)據(jù)鏈路層協(xié)議, 基于交錯(cuò)位協(xié)議(Alternating Bit Protocol, ABP), 并允許以塊的形式(如文件的某一部分)進(jìn)行有限次重傳, 采用了有確認(rèn)的停等策略, 類(lèi)似于ARQ機(jī)制: 發(fā)送方在發(fā)送一幀數(shù)據(jù)后, 等待對(duì)方應(yīng)答; 當(dāng)接收方收到一個(gè)正確的數(shù)據(jù)幀后, 向發(fā)送方發(fā)送一個(gè)確認(rèn)幀; 當(dāng)發(fā)送方收到此確認(rèn)幀后才能發(fā)送一個(gè)新的數(shù)據(jù)幀. 同時(shí), 收發(fā)雙方都使用了計(jì)時(shí)器以保證其實(shí)時(shí)性, 并限定了最大重傳次數(shù), 其流程類(lèi)似于X.25協(xié)議中的LAPB鏈路控制過(guò)程[3]. 文獻(xiàn)[4]應(yīng)用基于進(jìn)程代數(shù)的μCRL對(duì)BRP進(jìn)行了形式化規(guī)約和分析, 并使用定理證明器Coq對(duì)協(xié)議性質(zhì)進(jìn)行了驗(yàn)證. 文獻(xiàn)[5]使用UPPAL和SPIN工具對(duì)BRP及協(xié)議相關(guān)性質(zhì)進(jìn)行了驗(yàn)證. 上述文獻(xiàn)均側(cè)重于對(duì)協(xié)議性質(zhì)的驗(yàn)證, 缺乏對(duì)協(xié)議相關(guān)參數(shù)的量化分析.

在節(jié)點(diǎn)不斷移動(dòng)、拓?fù)鋭?dòng)態(tài)變化、帶寬受到限制的Ad Hoc網(wǎng)絡(luò)中, 節(jié)點(diǎn)間的通信受到收發(fā)節(jié)點(diǎn)間相鄰概率、信道質(zhì)量等因素的影響. BRP在Ad Hoc網(wǎng)絡(luò)環(huán)境下的研究較少. 基于此, 本文應(yīng)用概率模型檢測(cè)技術(shù),對(duì)Ad Hoc網(wǎng)絡(luò)環(huán)境中的BRP進(jìn)行了建模, 通過(guò)一定的概率來(lái)描述信道的不可靠性, 并用PRISM[6]工具量化分析了節(jié)點(diǎn)間信道質(zhì)量、文件的分組數(shù)和重傳的最大次數(shù)對(duì)網(wǎng)絡(luò)通信的影響, 驗(yàn)證了協(xié)議相關(guān)性質(zhì), 分析結(jié)果有助于根據(jù)網(wǎng)絡(luò)實(shí)際情況設(shè)置協(xié)議各參數(shù), 從而提高網(wǎng)絡(luò)性能.

1 Ad Hoc網(wǎng)絡(luò)中有限重傳協(xié)議的建模

1.1 協(xié)議描述

BRP由發(fā)送方S (Sender)、接收方R (Receiver)以及兩個(gè)按照FIFO方式處理數(shù)據(jù)的不可靠信道M (用于發(fā)送數(shù)據(jù)幀)和A (用于發(fā)送確認(rèn)幀)組成, 其原理如圖1所示, 其中REQ、CONF、E、F、G、H和IND均為通信端口, t1和t2分別為發(fā)送方和接收方的定時(shí)器.

BRP提供了發(fā)送方的請(qǐng)求服務(wù)、確認(rèn)服務(wù), 接收方的指示服務(wù)這三類(lèi)服務(wù)原語(yǔ), 分別表示如下:

(1) REQ(s)

請(qǐng)求服務(wù)負(fù)責(zé)以獨(dú)立數(shù)據(jù)幀的形式來(lái)發(fā)送一定長(zhǎng)度的數(shù)據(jù).

(2) CONF(c) (c∈{C_OK, C_NOK, C_DK})

確認(rèn)服務(wù)負(fù)責(zé)將請(qǐng)求服務(wù)的結(jié)果告知發(fā)送方.

C_OK: 成功發(fā)送請(qǐng)求信息;

C_NOK: 未能完全發(fā)送請(qǐng)求信息;

C_DK: 不能確定是否處理完請(qǐng)求信息. 僅當(dāng)已發(fā)送最后一幀但沒(méi)有收到確認(rèn)幀時(shí)才會(huì)出現(xiàn)這一情況.

(3) IND(d, i) (d是一個(gè)數(shù)據(jù), i∈{I_FST, I_INC, I_OK})

指示服務(wù)負(fù)責(zé)判斷數(shù)據(jù)幀的序號(hào), 并將新的數(shù)據(jù)幀發(fā)送給接收方.

I_FST: 收到的數(shù)據(jù)幀為第一幀;

I_INC: 收到的數(shù)據(jù)幀為中間幀;

I_OK: 收到的數(shù)據(jù)幀為最后一幀, 此時(shí)文件塊已傳送完畢.

(4) IND_NOT_OK

當(dāng)通信發(fā)生故障時(shí), 接收方只收到部分消息, 此服務(wù)原語(yǔ)則負(fù)責(zé)將故障情況告知發(fā)送方.

在此協(xié)議中, 將文件劃分為N ( N ＞2)塊, N = 1時(shí)協(xié)議等價(jià)于ABP. 初始時(shí)重傳計(jì)數(shù)器為0, 其最大值為MAX; 消息經(jīng)信道M和A傳送后, 以一定的概率正確到達(dá)或發(fā)生丟失. 信道M所發(fā)送的數(shù)據(jù)幀由三個(gè)比特位和數(shù)據(jù)塊組成, 其格式為(first, last, toggle, data); 相應(yīng)地, 信道A所發(fā)送的確認(rèn)幀格式為(first, last, toggle), 可以將其看作是數(shù)據(jù)幀除去數(shù)據(jù)后的頭部信息. 其中first和last是布爾變量, 取1時(shí)(true)分別表示此幀為所傳送文件的第一幀和最后一幀; toggle是布爾變量, 為幀標(biāo)志位, 接收方保存當(dāng)前toggle值用于區(qū)別后續(xù)數(shù)據(jù)幀以避免重復(fù), 初始值為0; data為數(shù)據(jù). 例如, 第一幀可表示為(1, 0, 0, d1).

圖1 BRP

在沒(méi)有幀丟失的正常通信情況下, 協(xié)議主要流程如下: 假設(shè)接收方R在發(fā)送傳送文件數(shù)據(jù)d1…dN的請(qǐng)求REQ(d1…dN)后啟動(dòng)定時(shí)器t2, 發(fā)送方S接收到此請(qǐng)求, 則通過(guò)端口E發(fā)送幀(1, 0, 0, d1), 并啟動(dòng)定時(shí)器t1. 信道M通過(guò)端口F將此幀傳送給R. 若在t2超時(shí)前收到此幀, R通過(guò)IND端口發(fā)送IND(d1, I_FST), 并在端口G處發(fā)送確認(rèn)幀(1,0,0), 保存此幀中的toggle位后重置定時(shí)器t2, 此確認(rèn)幀通過(guò)信道A到達(dá)端口H.在t1超時(shí)之前收到確認(rèn)后, S將發(fā)送第二個(gè)數(shù)據(jù)幀(0,0,1,d2), 此幀將前一數(shù)據(jù)幀中toggle這一標(biāo)志位置反,即為1, 并重置定時(shí)器t1; 若發(fā)生超時(shí), 重發(fā)此幀, 并將重傳計(jì)數(shù)器加1(若重傳計(jì)數(shù)器超過(guò)其最大值MAX, 則文件傳送失敗). 類(lèi)似地, 在t2超時(shí)之前收到第二幀后, 接收方發(fā)送IND(d2, I_INC)和確認(rèn)幀(0, 0, 1), 保存此幀中toggle位后重置定時(shí)器. 重復(fù)此過(guò)程, 直到最后一幀發(fā)送完畢, 此時(shí)數(shù)據(jù)幀為(0,1,?toggleN-1,dN), 接收方發(fā)送IND(dN, I_OK)和確認(rèn)幀(0,1,?toggleN-1), 并報(bào)告完成文件傳送和確認(rèn).然后, 發(fā)送方將發(fā)送CONF(C_OK), 報(bào)告文件傳送成功.

1.2 協(xié)議分析與建模

在通信過(guò)程中, 若數(shù)據(jù)幀或確認(rèn)幀發(fā)生丟失, 從發(fā)送方的角度進(jìn)行分析如下. 當(dāng)發(fā)送方S發(fā)送數(shù)據(jù)幀時(shí), 啟動(dòng)定時(shí)器t1, 等待接收方R的確認(rèn). 若在t1超時(shí)前收到確認(rèn), 則重置定時(shí)器并發(fā)送新的數(shù)據(jù)幀; 若t1超時(shí)且沒(méi)收到確認(rèn), 則重傳幀; 若已經(jīng)達(dá)到最大重傳次數(shù), 發(fā)送方則放棄傳送. 若在傳送最后一個(gè)數(shù)據(jù)幀時(shí)發(fā)生故障, 則調(diào)用CONF(C_DK)這一確認(rèn)服務(wù), 判斷是最后一個(gè)數(shù)據(jù)幀丟失以至沒(méi)有收到, 還是此幀的確認(rèn)幀丟失; 否則若在傳送過(guò)程中發(fā)生故障, 則調(diào)用CONF(C_NOK)確認(rèn)文件傳送失敗.

下面從接收方的角度來(lái)分析幀丟失的情況, 在此假定第一個(gè)數(shù)據(jù)幀不會(huì)發(fā)生丟失. 當(dāng)收到一個(gè)數(shù)據(jù)幀時(shí), 接收方對(duì)此幀進(jìn)行確認(rèn). 此數(shù)據(jù)幀中toggle位與前一幀中toggle位取值不同時(shí), 則此幀為新幀. 發(fā)送確認(rèn)后啟動(dòng)計(jì)時(shí)器t2, 并進(jìn)入等待狀態(tài). 若t2超時(shí)且沒(méi)有收到數(shù)據(jù)幀, 則調(diào)用IND_NOT_OK. 僅當(dāng)發(fā)送方終止傳送時(shí), 才會(huì)發(fā)生超時(shí). 在通信中斷一定時(shí)間后, S和R將重新同步啟動(dòng). 考慮信道傳輸延時(shí)(Channel Delay, CD), 從上述分析中可知, t2＞ max (t1+ CD), 這樣才能保證R能有足夠時(shí)間對(duì)接收的數(shù)據(jù)幀進(jìn)行處理.

在Ad Hoc網(wǎng)絡(luò)中, 節(jié)點(diǎn)間的通信受到收發(fā)節(jié)點(diǎn)間相鄰概率、信道質(zhì)量等因素的影響. 為了便于建模,對(duì)Ad Hoc網(wǎng)絡(luò)及協(xié)議進(jìn)行如下假設(shè):

(1)網(wǎng)絡(luò)面積為A, A = 1000×1000(m2), 移動(dòng)節(jié)點(diǎn)隨機(jī)分布其中, 并獨(dú)立地自由移動(dòng);

(2)節(jié)點(diǎn)的有效傳輸半徑為R, R = 250(m), 處于有效傳輸范圍內(nèi)的節(jié)點(diǎn)間可以直接通信. 在此不考慮噪聲的影響.

(3)信道M丟失數(shù)據(jù)幀的概率為1-q1, 信道A丟失確認(rèn)幀的概率為1-q2.

由上述假設(shè)可知, 收發(fā)節(jié)點(diǎn)處于有效傳輸范圍內(nèi)的概率為πR2/A. 根據(jù)BRP的執(zhí)行流程, 可以得出協(xié)議中各組件的有限狀態(tài)機(jī)如下.

圖2 BRP中發(fā)送方S的有限狀態(tài)機(jī)

BRP中發(fā)送方S的有限狀態(tài)機(jī)如圖2所示. 其中idle為空閑狀態(tài), next_frame為發(fā)送新數(shù)據(jù)幀狀態(tài), wait_ack為等待確認(rèn)幀狀態(tài), retransmit為重傳數(shù)據(jù)幀狀態(tài), success為發(fā)送成功狀態(tài), error為發(fā)送失敗狀態(tài), wait_sync為等待同步狀態(tài).

初始時(shí)S處于idle狀態(tài), 當(dāng)收到發(fā)送信息請(qǐng)求時(shí), 就進(jìn)入next_frame狀態(tài)開(kāi)始發(fā)送新的數(shù)據(jù)幀, 同時(shí)啟動(dòng)定時(shí)器. 發(fā)送之后進(jìn)入wait_ack狀態(tài), 等待R的確認(rèn)信息. 若在超時(shí)之前收到確認(rèn), 則發(fā)送成功進(jìn)入success狀態(tài), 接著發(fā)送下一個(gè)數(shù)據(jù)幀, 重復(fù)此過(guò)程, 若發(fā)送完畢就進(jìn)入idle狀態(tài); 若超時(shí)且沒(méi)有收到確認(rèn)幀, 則進(jìn)入restransmit狀態(tài)進(jìn)行重發(fā); 若重發(fā)次數(shù)超過(guò)最大值MAX, 則放棄傳送進(jìn)入error狀態(tài), 同步之后進(jìn)入idle狀態(tài).

BRP中接收方R的有限狀態(tài)機(jī)如圖3所示. 其中new_file為等待接收數(shù)據(jù)幀狀態(tài), fst_safe為判斷是否為第一個(gè)數(shù)據(jù)幀的狀態(tài), frame_received為數(shù)據(jù)幀接收狀態(tài), frame_reported為報(bào)告情況狀態(tài), idle為空狀態(tài), resync為同步狀態(tài).

圖3 BRP中接收方R的有限狀態(tài)機(jī)

初始時(shí)R處于new_file狀態(tài), 接收數(shù)據(jù)幀后相繼進(jìn)入fst_safe和frame_received狀態(tài). 此數(shù)據(jù)幀可能是第一幀、中間幀或最后一幀, 因而R對(duì)此進(jìn)行判斷進(jìn)入frame_reported狀態(tài), 并將結(jié)果輸出到IND端口. 然后將確認(rèn)信息反饋給S, 進(jìn)入idle狀態(tài),同時(shí)判斷所接收的前一數(shù)據(jù)幀是否為文件最后一幀并記錄其標(biāo)志位. 若沒(méi)有接收完畢, 繼續(xù)等待接收, 并根據(jù)標(biāo)志位判斷是否為重復(fù)幀. 如接收的數(shù)據(jù)幀是最后一個(gè), 則此次文件傳送完成, 等待同步之后, 可以再次開(kāi)始新的文件傳送; 若長(zhǎng)時(shí)間等待后仍沒(méi)收到S方響應(yīng), 則報(bào)告文件傳送失敗, 等待同步后重新接收.

圖4 信道M的概率有限狀態(tài)機(jī)

圖5 信道A的概率有限狀態(tài)機(jī)

圖6 Checker的有限狀態(tài)機(jī)

信道M、A只有三個(gè)狀態(tài), 即空閑狀態(tài)idle、發(fā)送狀態(tài)send和丟棄狀態(tài)lost. 信道M和A的成功發(fā)送概率分別是q1和q2, 即丟棄信息的概率分別為1-q1和1-q2. 新文件檢測(cè)器(Checker)則用于啟動(dòng)新文件的傳送.

2 協(xié)議相關(guān)參數(shù)及部分代碼

為了描述協(xié)議中各組件的非確定的概率行為, 將其建模為馬爾可夫決策過(guò)程(Markov Decision Processes, MDP), 每一組件用PRISM的一個(gè)模塊表示, 協(xié)議相關(guān)參數(shù)及部分代碼如下:

3 結(jié)果分析

使用PRISM對(duì)BRP進(jìn)行驗(yàn)證, 結(jié)果分析如下:

(1) 發(fā)送方報(bào)告不確定文件是否成功傳送而接收方得到文件完整信息的最大概率

圖7 參數(shù)MAX、N、q1、q2中其一變化而其它三個(gè)不變時(shí)的最大概率

該性質(zhì)可規(guī)約為Pmax=?[true U (srep=NOK & rrep=OK & recv=true)], 結(jié)果如圖7所示. 發(fā)送方報(bào)告不確定文件是否成功傳送而接收方得到文件完整信息的狀態(tài)是不可達(dá)的, 其最大概率始終是0, 不隨參數(shù)MAX、N、q1、q2的變化而變化. 同理, 發(fā)送方報(bào)告文件傳送成功而接收方?jīng)]有得到文件完整信息的概率的最大概率也為0. 由此可知, 協(xié)議具有安全性. 此外, 若接收節(jié)點(diǎn)不可靠(如一些惡意節(jié)點(diǎn), 正確接收卻報(bào)告錯(cuò)誤等), 可推知會(huì)破壞協(xié)議安全性, 在此不再作分析.

(2)發(fā)送方報(bào)告文件傳送成功的最大概率

圖8 發(fā)送方報(bào)告文件傳送成功的最大概率

該性質(zhì)可規(guī)約為Pmax=?[true U (srep=OK & T=true)]. 同理, 發(fā)送方報(bào)告文件傳送失敗這一性質(zhì)可規(guī)約為Pmax=?[ true U (s=error & T=true)]. 由圖8可知, 發(fā)送方報(bào)告?zhèn)魉统晒Φ淖畲蟾怕孰S著MAX、q1、q2的增大而增大, 隨N的增大而減少. 這是因?yàn)橹貍鞯拇螖?shù)越大, 信道的傳輸質(zhì)量越好, 數(shù)據(jù)傳送成功的概率則越大; 而一個(gè)文件的分組數(shù)N增大時(shí), 其傳輸效率降低, 因而不宜過(guò)大.

(3)發(fā)送方報(bào)告不確定文件是否成功傳送的概率

圖9 發(fā)送方報(bào)告不確定文件是否成功傳送的最大概率

該性質(zhì)可規(guī)約為Pmax=?[true U (s=error & T=true & srep=DK)], 這一性質(zhì)描述了信道質(zhì)量對(duì)協(xié)議性能的影響. 如圖9所示, 發(fā)送方報(bào)告不確定文件是否成功傳送的最大概率隨著MAX、N的增大總體趨于減小,隨著q1、q2的增大而增大.

(4)接收方不能接收任何數(shù)據(jù)而發(fā)送方仍試圖發(fā)送數(shù)據(jù)的最大概率

圖10 接收方不能接收任何數(shù)據(jù)而發(fā)送方仍試圖發(fā)送數(shù)據(jù)的最大概率

該性質(zhì)可規(guī)約為Pmax=?[true U ( srep!=0 & T=true & recv=false)], 這一性質(zhì)描述了協(xié)議正確完成的情況.由圖10可知, 接收方不能接收任何數(shù)據(jù)而發(fā)送方仍試圖發(fā)送數(shù)據(jù)的最大概率隨著MAX的值增大而減少,即協(xié)議正確完成的概率越高, 具有一定的活性; 隨著q1、q2的增大而減小, 且不隨N的變化而變化.

[1] Helmink L, Sellink M P A, Vaandrager F W.Proof Checking a Data Link Protocol[J]. In Proceedings Types for Proofs and Programs (TYPES'93), 1994: 127～165

[2] D'Argenio P R, Jeannet B, Jensen H E, et al.Reachability Analysis of Probabilistic Systems by Successive Refinements[J]. In Proceedings PAPM-PROBMIV'01, 2001: 39～56

[3] CCITT Fascicle VIII.3. CCCITT Recommendation X.25:Interface betweenDTEandDCEfor Terminals Operating in the Packet Mode on Public Data Networks[S], 1998.

[4] Groote J F, Pol J V D.A Bounded Retransmission Protocol for Large Data Packets[A]. AMAST'96[C]. 1996: 536～550

[5] D'Argenio P R, Katoen J P, Ruys T, et al.Modeling and Verifying a Bounded Retransmission Protocol[A]. In Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design[C]. 1996: 114～127

[6] Kwiatkowska M, Norman G, Parker D.www.cs.bham.ac.uk/～dxp/prism[EB/OL]

Modeling and Analysis of Bounded Retransmission Protocol in the Ad Hoc Network

CHEN Li-bin1, WEN Ying2
1. College of Computer Science, Hunan Institute of science and technology, Yueyang 414006, China 2. China Mobile Communication, Guangxi Nanning Corporation, Nanning 530028, China)

TP393

A

1672-5298(2010)01-0039-06

2010-12-12

陳立斌(1974- ), 男, 湖南武岡人, 湖南理工學(xué)院計(jì)算機(jī)學(xué)院講師. 主要研究方向: 網(wǎng)絡(luò)技術(shù)