陳立斌, 文 英

(1. 湖南理工學院 計算機學院, 湖南 岳陽 414006; 中國移動集團廣西有限公司 南寧分公司, 南寧 530028)

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

陳立斌1, 文 英2

(1. 湖南理工學院 計算機學院, 湖南 岳陽 414006; 中國移動集團廣西有限公司 南寧分公司, 南寧 530028)

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

有限重傳協(xié)議; Ad Hoc網(wǎng)絡(luò); 概率模型檢測; 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é)議, 基于交錯位協(xié)議(Alternating Bit Protocol, ABP), 并允許以塊的形式(如文件的某一部分)進行有限次重傳, 采用了有確認的停等策略, 類似于ARQ機制: 發(fā)送方在發(fā)送一幀數(shù)據(jù)后, 等待對方應(yīng)答; 當接收方收到一個正確的數(shù)據(jù)幀后, 向發(fā)送方發(fā)送一個確認幀; 當發(fā)送方收到此確認幀后才能發(fā)送一個新的數(shù)據(jù)幀. 同時, 收發(fā)雙方都使用了計時器以保證其實時性, 并限定了最大重傳次數(shù), 其流程類似于X.25協(xié)議中的LAPB鏈路控制過程[3]. 文獻[4]應(yīng)用基于進程代數(shù)的μCRL對BRP進行了形式化規(guī)約和分析, 并使用定理證明器Coq對協(xié)議性質(zhì)進行了驗證. 文獻[5]使用UPPAL和SPIN工具對BRP及協(xié)議相關(guān)性質(zhì)進行了驗證. 上述文獻均側(cè)重于對協(xié)議性質(zhì)的驗證, 缺乏對協(xié)議相關(guān)參數(shù)的量化分析.

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

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

1.1 協(xié)議描述

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

BRP提供了發(fā)送方的請求服務(wù)、確認服務(wù), 接收方的指示服務(wù)這三類服務(wù)原語, 分別表示如下:

(1) REQ(s)

請求服務(wù)負責以獨立數(shù)據(jù)幀的形式來發(fā)送一定長度的數(shù)據(jù).

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

確認服務(wù)負責將請求服務(wù)的結(jié)果告知發(fā)送方.

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

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

C_DK: 不能確定是否處理完請求信息. 僅當已發(fā)送最后一幀但沒有收到確認幀時才會出現(xiàn)這一情況.

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

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

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

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

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

(4) IND_NOT_OK

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

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

圖1 BRP

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3 結(jié)果分析

使用PRISM對BRP進行驗證, 結(jié)果分析如下:

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

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

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

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

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

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

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

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

該性質(zhì)可規(guī)約為Pmax=?[true U (s=error & T=true & srep=DK)], 這一性質(zhì)描述了信道質(zhì)量對協(xié)議性能的影響. 如圖9所示, 發(fā)送方報告不確定文件是否成功傳送的最大概率隨著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- ), 男, 湖南武岡人, 湖南理工學院計算機學院講師. 主要研究方向: 網(wǎng)絡(luò)技術(shù)