停等式ARQ協(xié)議的SPIN模型檢測(cè)

(福建工程學(xué)院 生態(tài)環(huán)境與城市建設(shè)學(xué)院， 福建 福州 350118)

隨著科學(xué)技術(shù)的快速發(fā)展，計(jì)算機(jī)網(wǎng)絡(luò)已滲透到社會(huì)的各個(gè)領(lǐng)域，并在日常生活中發(fā)揮著越來(lái)越重要的作用。作為計(jì)算機(jī)與網(wǎng)絡(luò)連接的標(biāo)準(zhǔn)，通信協(xié)議已是網(wǎng)絡(luò)發(fā)揮作用的基礎(chǔ)，如何保證其可靠性和安全性成為一個(gè)熱門的研究問(wèn)題。早期的通信協(xié)議大多采用自然語(yǔ)言進(jìn)行描述，但由于自然語(yǔ)言自身存在的模糊性和二義性等局限，導(dǎo)致通信協(xié)議容易出現(xiàn)錯(cuò)誤。因此，越來(lái)越多的研究人員開(kāi)始關(guān)注通信協(xié)議的形式化描述與驗(yàn)證，并促使通信協(xié)議成為一種更為嚴(yán)謹(jǐn)?shù)囊?guī)范。但是，如何對(duì)通信協(xié)議進(jìn)行建模并完成安全檢測(cè)仍然是一件非常困難的工作，且不同通訊協(xié)議在建模、驗(yàn)證及性能分析等各方面或階段的表現(xiàn)也大相徑庭[1]。在眾多通信協(xié)議中，停等式自動(dòng)請(qǐng)求重傳(auto repeat request, ARQ)協(xié)議是數(shù)據(jù)通信網(wǎng)絡(luò)中最常見(jiàn)的差錯(cuò)控制協(xié)議之一。因此，識(shí)別停等式ARQ存在的弱點(diǎn)有助于改進(jìn)當(dāng)前網(wǎng)絡(luò)協(xié)議的不足，從而提高數(shù)據(jù)通信的安全性。

1 停等式ARQ協(xié)議

在數(shù)據(jù)通信網(wǎng)絡(luò)中，自動(dòng)請(qǐng)求重傳協(xié)議常被用于處理信道中的差錯(cuò)控制。ARQ通過(guò)接收端請(qǐng)求發(fā)送端重新傳輸錯(cuò)誤數(shù)據(jù)報(bào)文的策略，實(shí)現(xiàn)報(bào)文在數(shù)據(jù)鏈路層的可靠傳輸。ARQ協(xié)議分成為3類[2]：(1)停等式ARQ，即每一幀確認(rèn)接收后再發(fā)送下一幀；(2)連續(xù)式ARQ，即一次發(fā)送多個(gè)幀后再確認(rèn)接收；(3)選擇性重傳ARQ，即有選擇地重傳出錯(cuò)幀?？梢钥闯?，以上3種ARQ協(xié)議的主要區(qū)別是對(duì)出錯(cuò)的數(shù)據(jù)報(bào)文的處理方式不同。從停等式ARQ至選擇性重傳ARQ，其復(fù)雜性遞增，效率也遞增。其中，停等式ARQ協(xié)議雖然最為簡(jiǎn)單，但應(yīng)用的范圍卻不小，尤其是在硬件無(wú)線通訊領(lǐng)域，由于其簡(jiǎn)單且易于實(shí)現(xiàn)而備受青睞[3]。

停等式ARQ協(xié)議的工作原理可按發(fā)送端和接收端分別進(jìn)行描述。對(duì)于發(fā)送端，它每發(fā)送完一幀便停止發(fā)送，并等待接收端的確認(rèn)。只有當(dāng)接收到了來(lái)自接收端的確認(rèn)幀之后，發(fā)送端才繼續(xù)發(fā)送下一幀。對(duì)于接收端，它每收到一個(gè)無(wú)差錯(cuò)的幀，便將其轉(zhuǎn)發(fā)給上層軟件，并向發(fā)送端發(fā)送確認(rèn)幀。若接收端收到有差錯(cuò)的幀，便直接丟棄該幀，而不做任何其他操作。因此，為了保證報(bào)文在數(shù)據(jù)鏈路層的可靠傳輸，發(fā)送端必須對(duì)所發(fā)送的幀進(jìn)行編號(hào)。由于發(fā)送端每次只發(fā)送一幀，因此停等式ARQ協(xié)議僅使用一個(gè)比特對(duì)幀進(jìn)行編號(hào)，即只有0號(hào)幀和1號(hào)幀兩種類型。發(fā)送端依次循環(huán)發(fā)送0號(hào)幀和1號(hào)幀，即先發(fā)送0號(hào)幀，再發(fā)送1號(hào)幀，再下次又發(fā)送0號(hào)幀，如此循環(huán)反復(fù)。接收端發(fā)送確認(rèn)幀時(shí)，則采用“ACKn”的格式來(lái)表示已經(jīng)正確接收到了第n-1號(hào)幀，當(dāng)前正在等待接收第n號(hào)幀。

對(duì)于報(bào)文在數(shù)據(jù)傳輸中可能出現(xiàn)的不同狀況，發(fā)送端和接收端將有不同的處理機(jī)制。如圖1所示，當(dāng)數(shù)據(jù)幀或確認(rèn)幀出現(xiàn)錯(cuò)誤，發(fā)送端和接收端會(huì)依據(jù)停等式ARQ協(xié)議執(zhí)行相應(yīng)的處理操作。

(1)正常情況下，發(fā)送端和接收端有序地發(fā)送數(shù)據(jù)幀和確認(rèn)幀。由于發(fā)送端只有在收到確認(rèn)幀的情況下才會(huì)發(fā)送下一次幀，所以接收端能夠及時(shí)接收所有的數(shù)據(jù)幀，數(shù)據(jù)在傳輸過(guò)程中不出會(huì)現(xiàn)延時(shí)或丟失。

(2)發(fā)送端發(fā)出的數(shù)據(jù)幀出錯(cuò)。在這種情況下，接收端將丟棄該幀，且不發(fā)送確認(rèn)幀。因此，如果系統(tǒng)要求發(fā)送端一定要收到接收端的確認(rèn)幀后才能發(fā)送下一幀，那么接收端在發(fā)送數(shù)據(jù)幀之后就會(huì)進(jìn)入等待，從而導(dǎo)致死鎖。為了解決這個(gè)問(wèn)題，系統(tǒng)可要求發(fā)送端每發(fā)送完一個(gè)幀，就啟動(dòng)一個(gè)計(jì)時(shí)器來(lái)計(jì)算等待時(shí)間。當(dāng)?shù)却龝r(shí)間超過(guò)了預(yù)先設(shè)定的重傳時(shí)間閾值，那么發(fā)送端便重新發(fā)送前一個(gè)數(shù)據(jù)幀。顯然，重傳時(shí)間閾值的設(shè)定會(huì)影響數(shù)據(jù)傳輸?shù)男?，因此?shù)據(jù)傳輸往往會(huì)有所延時(shí)。

(3)發(fā)送端發(fā)出的數(shù)據(jù)幀正確，而確認(rèn)幀發(fā)生異常。在這種情況下，發(fā)送端無(wú)法正確接收到確認(rèn)幀。當(dāng)?shù)却龝r(shí)間超過(guò)重傳時(shí)間，發(fā)送端將重新發(fā)傳前一幀。然而，當(dāng)接收端收到這個(gè)重復(fù)幀時(shí)，它將丟棄該幀，并再次發(fā)送確認(rèn)幀。由此可發(fā)現(xiàn)，一旦沒(méi)有對(duì)數(shù)據(jù)幀進(jìn)行編號(hào)，就可能導(dǎo)致接收端無(wú)法確認(rèn)收到的幀是否重復(fù)。

圖1 停等式ARQ協(xié)議工作原理Fig.1 Working principle of the stop-and-wait ARQ

2 Promela語(yǔ)言建模

SPIN是一種著名的分析驗(yàn)證并發(fā)系統(tǒng)邏輯一致性的模型檢測(cè)工具[4]，它所提供的系統(tǒng)建模語(yǔ)言Promela能夠用于直觀且明確地對(duì)有限狀態(tài)系統(tǒng)進(jìn)行建模。除了允許動(dòng)態(tài)創(chuàng)建并行的進(jìn)程之外，Promela還能夠在進(jìn)程之間進(jìn)行同步和異步通信。

2．1 消息傳遞的建模

停等式ARQ協(xié)議是用于保證數(shù)據(jù)有序、可靠傳遞的協(xié)議，因此對(duì)消息傳遞的模擬是必不可少的。Promela語(yǔ)言提供了一種先進(jìn)先出的消息通道的機(jī)制，來(lái)模擬消息在進(jìn)程之間的傳遞。通道的容量可以任意確定，同時(shí)每個(gè)消息可以包含多個(gè)變量。本文采用消息在通道內(nèi)的傳遞來(lái)模擬幀在信道中的傳輸。

在停等式ARQ協(xié)議中，對(duì)于發(fā)送端而言，每個(gè)幀要包含消息的編號(hào)和內(nèi)容。同時(shí)，為了模擬幀的正確傳輸和錯(cuò)誤傳輸?shù)膬煞N不同情況，還應(yīng)包含一個(gè)幀的狀態(tài)標(biāo)記，區(qū)別正確傳送的幀和錯(cuò)誤傳送的幀。對(duì)于接收端而言，它所傳遞的消息需要包含確認(rèn)編號(hào)ACKn，同樣為了模擬確認(rèn)幀的正確傳輸和錯(cuò)誤傳輸?shù)膬煞N不同情況，確認(rèn)幀中也應(yīng)該包含一個(gè)幀的狀態(tài)標(biāo)記。參考文獻(xiàn)[5]的描述方法, 本文將幀的狀態(tài)和通道標(biāo)記定義如下：

mtype={mesg, ack, err}; chan s_r=[10] of {mtype, dbyte, mbyte}; chan r_s=[10] of {mtype, dbyte, mbyte}。

其中，mesg、ack和err分別代表該幀是消息幀、確認(rèn)幀或者錯(cuò)誤幀。通道s_r用于模擬發(fā)送端向接收端發(fā)送數(shù)據(jù)幀所使用的信道，通道r_s則模擬接收端向發(fā)送端發(fā)送確認(rèn)幀所使用的信道。通道中所傳輸?shù)拿總€(gè)消息都包含3個(gè)域，mtype代表幀的狀態(tài)標(biāo)記，dbyte和mbyte分別代表數(shù)據(jù)和幀編號(hào)。

此外，本文在發(fā)送端使用out!msg(o,s)和out!err(0,0)來(lái)模擬數(shù)據(jù)幀的正確傳輸和錯(cuò)誤傳輸兩種情況。在接收端，則使用out!ack(0, es)和out!err(0, 0)來(lái)模擬確認(rèn)幀的正確傳輸和錯(cuò)誤傳輸兩種情況。

2．2 超時(shí)重傳機(jī)制的建模

在停等式ARQ協(xié)議中，出現(xiàn)超時(shí)的情況只有數(shù)據(jù)幀丟失、數(shù)據(jù)幀出錯(cuò)、確認(rèn)幀丟失和確認(rèn)幀出錯(cuò)4種：

(1)數(shù)據(jù)幀丟失：接收端收不到數(shù)據(jù)幀就不會(huì)發(fā)送確認(rèn)幀，導(dǎo)致超時(shí)。

(2)數(shù)據(jù)幀出錯(cuò)：接收端接收到錯(cuò)誤的數(shù)據(jù)幀，將出錯(cuò)的數(shù)據(jù)幀丟棄，不發(fā)送確認(rèn)幀，導(dǎo)致超時(shí)。

(3)確認(rèn)幀丟失：發(fā)送端收不到確認(rèn)幀，導(dǎo)致超時(shí)。

(4)確認(rèn)幀出錯(cuò)：發(fā)送端收到錯(cuò)誤的確認(rèn)幀，將出錯(cuò)的確認(rèn)幀丟棄，導(dǎo)致超時(shí)。

為了標(biāo)識(shí)以上不同情況，本文設(shè)置了一個(gè)byte類型的變量to作為超時(shí)標(biāo)記。當(dāng)它的值為1時(shí)，表示會(huì)出現(xiàn)傳輸超時(shí)的情況，進(jìn)而啟動(dòng)重傳選項(xiàng)。在數(shù)據(jù)丟失、出錯(cuò)和確認(rèn)幀丟失時(shí)，就將to的值賦為1，并啟動(dòng)重傳。當(dāng)發(fā)送端接收到出錯(cuò)的確認(rèn)幀時(shí)，直接啟動(dòng)重傳。

2．3 發(fā)送端建模

為了證明數(shù)據(jù)幀是被有序傳遞的，可在數(shù)據(jù)幀所傳送的數(shù)據(jù)o設(shè)置為一個(gè)從0遞增到MAX-1的量。如果所有的數(shù)據(jù)幀都被正確且有序地送到了接收端，則數(shù)據(jù)幀中o的值就應(yīng)該是有序遞增。因此，可對(duì)發(fā)送端建模如下：

模型1 發(fā)送端模型

proctype sender(chan in,out)

{

int o;

byte s, r;

o = MAX-1;

s = 0;

do

/*讓待傳送的數(shù)據(jù)遞增*/

::o=(o+1) % MAX;

again:if

/*模擬數(shù)據(jù)幀的正確傳送*/

::out!mesg(o,s);

/*模擬數(shù)據(jù)幀的錯(cuò)誤傳送*/

::out!err(0,0); cnt++;}

/*模擬數(shù)據(jù)幀丟失，啟動(dòng)重傳選項(xiàng)*/

::to = 1;

fi

if

::(to == 1) ->

atomic{to = 0; goto again}

/*接收到出錯(cuò)的確認(rèn)幀，重傳*/

::in?err(0,0); -> goto again;

/*接收到正確的確認(rèn)幀，修改幀編號(hào)*/

::in?ack(0, r) ->

s = 1 - s;assert (s == r);

fi

od

}

2．4 接收端建模

本文設(shè)置了變量ei和es來(lái)分別代表預(yù)期數(shù)據(jù)和預(yù)期幀編號(hào)。當(dāng)接收端接收的數(shù)據(jù)幀編號(hào)是正確的，則修改預(yù)期幀編號(hào)es，并發(fā)送確認(rèn)幀。由于發(fā)送的確認(rèn)幀可能在傳輸過(guò)程中出現(xiàn)正確傳輸、錯(cuò)誤傳輸和丟失3種情況，因此采用以下方式分別對(duì)錯(cuò)誤傳輸和丟失進(jìn)行模擬：(1)當(dāng)確認(rèn)幀丟失的情況，將超時(shí)標(biāo)記to賦值為1；(2)如果該幀的編號(hào)不正確，則不修改預(yù)期幀編號(hào)es，而是再發(fā)送一次確認(rèn)幀。因此，可對(duì)接收端的建模如下：

模型2 接收端模型

proctype receiver(chan in,out)

{

int i, ei;

byte s, es;

ei = 0;

es = 0;

do

::in?mesg(i,s);->

if

/*數(shù)據(jù)幀編號(hào)正確*/

::( s == es)->

es= (es + 1) % MAX;

ei=(ei+1) % MAX;

if

/*模擬確認(rèn)幀的正確傳送*/

::out!ack(es,0);

/*模擬數(shù)據(jù)幀的錯(cuò)誤傳送*/

::out!err(0,0);

::to=1;

fi

::(s != es)->

if

/*再次傳送確認(rèn)幀*/

::out!ack(0, es);

::out!err(0, 0);

::to = 1;

fi

fi

/*接收到錯(cuò)誤的數(shù)據(jù)幀，啟動(dòng)重傳選項(xiàng)*/

::in?err(0,0)->to = 1;

od

}

2．5 主進(jìn)程建模

最后，在得到發(fā)送端模型sender和接收端receiver的基礎(chǔ)上，可構(gòu)建主進(jìn)程模型init，創(chuàng)建上述兩個(gè)進(jìn)程的實(shí)例，并給它們傳遞通道：

模型3 主進(jìn)程模型

proctype init()

{

chan s_r = [10] of {mtype, int, byte};

chan r_s = [10] of {mtype, int, byte};

atomic

{

run sender (r_s, s_r);

run receiver (s_r, r_s)

}

}

3 SPIN模型檢測(cè)

停等式ARQ協(xié)議主要是用于實(shí)現(xiàn)數(shù)據(jù)的有序、可靠的傳遞?；谖墨I(xiàn)[5]所構(gòu)建的模型以及文獻(xiàn)[6]所描述的帶參性質(zhì)形式化描述方法的基礎(chǔ)上，本文從發(fā)送端行為、接收端行為和活性3個(gè)方面進(jìn)一步驗(yàn)證所建模型是否正確。

3.1 發(fā)送端行為

如果協(xié)議是正確的，發(fā)送方總是處于這樣的狀態(tài)：已發(fā)送完0號(hào)數(shù)據(jù)幀正在等待1號(hào)確認(rèn)幀，或已發(fā)送完1號(hào)數(shù)據(jù)幀正在等待0號(hào)確認(rèn)幀?？梢酝ㄟ^(guò)檢驗(yàn)sender進(jìn)程中數(shù)據(jù)幀的編號(hào)和確認(rèn)幀的編號(hào)來(lái)檢測(cè)這個(gè)性質(zhì)。輸入以下LTL語(yǔ)句進(jìn)行檢測(cè)：

#define cdn1 (cnt == 0)

#define cdn2 ((r == 0 && s == 1) || (r == 1 && s == 0))

cdn1-><>cdn2

檢測(cè)結(jié)果為“erros :0”，這說(shuō)明在任何時(shí)刻，發(fā)送方已發(fā)送的數(shù)據(jù)幀的編號(hào)與等待接收的確認(rèn)幀的編號(hào)都是不相等的。

3.2 接收端行為

如果協(xié)議是正確的，接收方總是處于這樣的狀態(tài)：已發(fā)送完0號(hào)確認(rèn)幀正在等待1號(hào)數(shù)據(jù)幀，或已發(fā)送完1號(hào)確認(rèn)幀正在等待0號(hào)數(shù)據(jù)幀。可以通過(guò)檢驗(yàn)reciever進(jìn)程中數(shù)據(jù)幀的編號(hào)和確認(rèn)幀的編號(hào)來(lái)檢測(cè)這個(gè)性質(zhì)。輸入以下LTL語(yǔ)句進(jìn)行檢測(cè)：

#define cdn1 (cnt == 0)

#define cdn3 ((s == 0 && es == 1) || (s == 1 && es == 0))

cdn1-><>cdn3

檢測(cè)結(jié)果為“erros :0”，這說(shuō)明在任何時(shí)刻，接收方已接收的數(shù)據(jù)幀的編號(hào)與要發(fā)送的確認(rèn)幀的編號(hào)都是不相等的。

3.3 活性

協(xié)議的活性是指協(xié)議運(yùn)行時(shí)一些好的事情會(huì)發(fā)生，比如預(yù)定的事情會(huì)產(chǎn)生、指定的狀態(tài)會(huì)到達(dá)、應(yīng)該進(jìn)行的協(xié)議活動(dòng)會(huì)進(jìn)行等。在這個(gè)協(xié)議中，活性是指發(fā)送方在給接收方發(fā)送數(shù)據(jù)后，接收方一定會(huì)給予應(yīng)答。接收方在接收數(shù)據(jù)后，通道內(nèi)的幀數(shù)量為0。而接收方在應(yīng)答后，會(huì)改變預(yù)期接收的數(shù)據(jù)ei，從而使其與已接收的數(shù)據(jù)i不同。輸入以下LTL語(yǔ)句進(jìn)行檢測(cè)：

#define cdn1 (cnt == 0)

#define cdn4 (ei != i)

cdn1->[]<>cdn4

檢測(cè)結(jié)果為“erros :0”，這說(shuō)明在任何時(shí)刻，接收方在接收到發(fā)送方傳送來(lái)的數(shù)據(jù)后，都會(huì)給予應(yīng)答。

4 攻擊者建模及檢測(cè)

停等式ARQ協(xié)議與其它的底層協(xié)議一樣，也是一種很脆弱的協(xié)議[7]。常見(jiàn)的對(duì)停等式ARQ協(xié)議攻擊方法有兩種，分別是對(duì)傳輸順序和對(duì)傳輸內(nèi)容的攻擊。針對(duì)這一問(wèn)題，本文使用Promela語(yǔ)言設(shè)計(jì)一個(gè)攻擊者的模型，隨機(jī)執(zhí)行以下兩種攻擊：

(1)對(duì)數(shù)據(jù)傳輸過(guò)程進(jìn)行一次攻擊：捕獲發(fā)送端發(fā)送的一個(gè)數(shù)據(jù)幀，并偽造一個(gè)確認(rèn)幀返回給發(fā)送端。

(2)攔截sender進(jìn)程的發(fā)送的一個(gè)數(shù)據(jù)幀，并將其偽造成一個(gè)重復(fù)幀發(fā)送給reciever進(jìn)程。然后，再冒充reciever進(jìn)程向sender進(jìn)程發(fā)送一個(gè)確認(rèn)幀。

由于假設(shè)數(shù)據(jù)有序遞增，因此可以很容易地計(jì)算出預(yù)期接收的數(shù)據(jù)。對(duì)這個(gè)性質(zhì)進(jìn)行檢測(cè)，要在接收到正確的數(shù)據(jù)幀、并確定該幀的編號(hào)正確后，加上一個(gè)斷言語(yǔ)句“assert(i == ei)”。因此，與上述攻擊者模型對(duì)應(yīng)的Promela語(yǔ)言模型可表述為：

模型4 攻擊者模型

proctype attack(chan in,out)

{

int i, ei;

byte s, es;

ei = 0;

es = 0;

do

/*攔截?cái)?shù)據(jù)幀*/

::atomic{in?mesg(i,s);cnt--}->

/*偽造確認(rèn)幀*/

es=1-s;

atomic{out!ack(0, es); cnt++};

break;

: :atomic{in?mesg(i,s);cnt--}->

es=1-s;

/*發(fā)送確認(rèn)幀和重復(fù)數(shù)據(jù)幀*/

atomic{in!mesg(i,1-s);

out!ack(0, es);}

od

}

使用該攻擊者模型對(duì)停等式ARQ協(xié)議在模型進(jìn)行攻擊，發(fā)現(xiàn)以下攻擊過(guò)程。attack進(jìn)程攔截了0號(hào)數(shù)據(jù)幀，偽造1號(hào)確認(rèn)幀發(fā)送給sender進(jìn)程，再將0號(hào)數(shù)據(jù)幀的編號(hào)改為1，發(fā)送給reciever進(jìn)程。receiver進(jìn)程被幀編號(hào)所欺騙，認(rèn)為這是一個(gè)重復(fù)的數(shù)據(jù)幀，將其丟棄，并重復(fù)發(fā)送0號(hào)確認(rèn)幀。sender進(jìn)程在收到偽造的1號(hào)確認(rèn)幀后，發(fā)送出1號(hào)數(shù)據(jù)幀，并期待0號(hào)數(shù)據(jù)幀。接著，重復(fù)發(fā)送的0號(hào)確認(rèn)幀到達(dá)，而sender進(jìn)程卻誤認(rèn)為1號(hào)數(shù)據(jù)幀已經(jīng)被正確接收，發(fā)出新的0號(hào)數(shù)據(jù)幀。這個(gè)新的0號(hào)數(shù)據(jù)幀被receiver進(jìn)程接收，結(jié)果造成接收的數(shù)據(jù)與期待的數(shù)據(jù)不一致，違背了斷言“assert(i == ei);”。這樣，attack進(jìn)程就成功地完成了一次攻擊，使傳輸過(guò)程出現(xiàn)了漏幀。一旦去掉斷言“assert(i == ei);”，傳輸過(guò)程雖然仍會(huì)正常進(jìn)行，但在傳輸過(guò)程中，attack進(jìn)程在不斷進(jìn)行攻擊，從而不斷地造成漏幀。更為嚴(yán)重的是，attack進(jìn)程在每一次攻擊都會(huì)攔截一個(gè)數(shù)據(jù)幀，并通過(guò)欺騙令發(fā)送和接收雙方都感覺(jué)不到，使傳輸持續(xù)進(jìn)行。但在傳輸結(jié)束后，接收方所接收到的數(shù)據(jù)卻是不完整的。

由上述的攻擊者模型可發(fā)現(xiàn)，對(duì)停等式ARQ協(xié)議的攻擊是很容易的，攻擊方只需要進(jìn)行簡(jiǎn)單的攔截和偽造就可以破壞整個(gè)傳輸過(guò)程。而且攻擊方所付出的代價(jià)是很微小的，不需要監(jiān)控整個(gè)傳輸過(guò)程，在任意時(shí)刻進(jìn)行攻擊都可以達(dá)到破壞傳輸?shù)哪康?。尤其是?duì)傳輸順序的攻擊，只需要進(jìn)行一次，就可以使整個(gè)傳輸過(guò)程停滯，浪費(fèi)大量的通信資源。

5 結(jié)語(yǔ)

本文介紹了停等式ARQ協(xié)議的模型檢測(cè)，并使用Promela語(yǔ)言對(duì)消息傳遞、超時(shí)重傳機(jī)制、發(fā)送端、接收端和主進(jìn)程都分別進(jìn)行建模。在此基礎(chǔ)上，從發(fā)送端行為、接收端行為和活性3個(gè)方面進(jìn)一步驗(yàn)證所建模型是否正確。最后，使用Promela語(yǔ)言設(shè)計(jì)一個(gè)攻擊者模型來(lái)模擬對(duì)停等式ARQ協(xié)議的攻擊行為。

參考文獻(xiàn)：

[1] 李新宇.用于通信網(wǎng)絡(luò)協(xié)議開(kāi)發(fā)的形式化方法[J].中國(guó)新通信,2014(15):100-101.

[2] LU D L, CHANG J F. Performance of ARQ protocols in nonindependent channel errors[J]. IEEE Trans Commun, 1993, 41(5): 721-730.

[3] 徐佑軍,譚敦茂,朱建武,等.藍(lán)牙無(wú)線鏈路質(zhì)量的分析、測(cè)試與改善[J].計(jì)算機(jī)工程與應(yīng)用,2004,40(12):129-131，211.

[4] HOLZMANN G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering,1997,23(5):279-295.

[5] 陳義,唐鄭熠.通信協(xié)議的Promela語(yǔ)言建模與檢測(cè)[J].福建電腦，2016,32(3):39-40.

[6] 徐永生.帶參性質(zhì)的形式化描述與證明[D].成都：電子科技大學(xué),2015.

[7] 吳勇,李祥.基于TLA的ARQ協(xié)議描述與驗(yàn)證[J].計(jì)算機(jī)安全,2012(8): 40-43.