通信協(xié)議分析-5-協(xié)議驗(yàn)證技術(shù)

第五章

協(xié)議驗(yàn)證技術(shù)協(xié)議驗(yàn)證(protocolverification):對(duì)協(xié)議本身的邏輯正確性進(jìn)行校驗(yàn)的過(guò)程。協(xié)議分析（protocolanalysis）協(xié)議綜合（protocolsynthesis）通常所說(shuō)的協(xié)議驗(yàn)證指的是協(xié)議分析。

協(xié)議綜合將協(xié)議設(shè)計(jì)過(guò)程和協(xié)議驗(yàn)證過(guò)程融合在一起。它通過(guò)一組能確保所設(shè)計(jì)的協(xié)議是正確的規(guī)則，從一些基本協(xié)議模塊（這些基本模塊已證明是正確的）中產(chǎn)生所希望的目標(biāo)協(xié)議。

協(xié)議分析的目的：對(duì)已設(shè)計(jì)的協(xié)議進(jìn)行分析和校驗(yàn)（這些已設(shè)計(jì)的協(xié)議大都是采用非形式化設(shè)計(jì)方法產(chǎn)生的）。

主要內(nèi)容5.1引言5.2基于CFSM的可達(dá)性分析

5.2.1CFSM 5.2.2窮盡可達(dá)性分析

5.2.3非窮盡可達(dá)性分析

5.2.4協(xié)議錯(cuò)誤檢測(cè)方法5.3不變性分析5.4基于FSM等價(jià)性分析5.1引言協(xié)議分析方法：可達(dá)性分析(reachabilityanalysis)

等價(jià)性分析(equivalenceanalysis)

不變性分析(invarianceanalysis)這些分析工作可以手工完成，但更重要的是確定算法之后，借助于分析工具在計(jì)算機(jī)中自動(dòng)或半自動(dòng)完成。5.1引言協(xié)議表達(dá)形式：

用自然語(yǔ)言描述的非形式化協(xié)議文本

用協(xié)議模型技術(shù)表達(dá)的協(xié)議模型

用形式描述語(yǔ)言描述的協(xié)議規(guī)范用程序設(shè)計(jì)語(yǔ)言描述的協(xié)議代碼上述分析方法在這幾種表達(dá)形式上都可進(jìn)行（手工或軟件工具）。然而，通常都在協(xié)議模型上進(jìn)行協(xié)議分析（簡(jiǎn)單，容易形成確定算法）。5.2基于CFSM的可達(dá)性分析基于CFSM模型的可達(dá)性分析，產(chǎn)生和檢查協(xié)議所有或部分可達(dá)狀態(tài)。所謂可達(dá)狀態(tài)指協(xié)議從初始狀態(tài)開始經(jīng)歷有限次轉(zhuǎn)換之后可達(dá)到的狀態(tài)，所有可達(dá)狀態(tài)構(gòu)成可達(dá)圖（reachabilitygraph）?？蛇_(dá)性分析的最重要工作是產(chǎn)生和檢查可達(dá)圖，判定是否存在死鎖、活鎖等協(xié)議錯(cuò)誤。5.2基于CFSM的可達(dá)性分析可達(dá)性分析涉及三個(gè)重要技術(shù)：怎樣找出所有可達(dá)狀態(tài)，構(gòu)成可達(dá)圖；怎樣檢測(cè)死鎖、活鎖等協(xié)議錯(cuò)誤；怎樣解決狀態(tài)爆炸問題。5.2.1CFSMC1C2+ASender21-R+R-AReceiver21CFSM

CFSM(CommunicatingFiniteStateMachine)用狀態(tài)、轉(zhuǎn)移和通道表示此處sender擁有兩個(gè)通道：C1和C2。類型均設(shè)為FIFO。

C1為輸出通道。C2為輸入通道。當(dāng)滿足輸出轉(zhuǎn)移條件，Sender通過(guò)C1將消息R發(fā)送給Receiver。當(dāng)且僅當(dāng)C2中存在消息A時(shí)，Sender啟動(dòng)接收轉(zhuǎn)移過(guò)程。CFSM12CSFM的初始狀態(tài)，每個(gè)CFSM只有一個(gè)初始狀態(tài)CFSM的狀態(tài)CFSM狀態(tài)轉(zhuǎn)移

-R發(fā)送R

+A接收A

此外還可以表示為：(1,2,-R)和(2,1,+A)-R2+A1C1C2+ASender21-R+R-AReceiver21當(dāng)前狀態(tài)當(dāng)協(xié)議啟動(dòng)時(shí)，Sender和Receiver各處于各自的初始狀態(tài)。處于狀態(tài)1的Receiver不能啟動(dòng)輸出轉(zhuǎn)移(1,2,+R)，處于狀態(tài)1的Sender可以啟動(dòng)輸出轉(zhuǎn)移(1,2,-R)，使Sender的當(dāng)前狀態(tài)轉(zhuǎn)移到2，消息R被放入通道C1。C1C2+ASender21-R+R-AReceiver21R5.2.1CFSM此時(shí)Sender處于狀態(tài)2，可執(zhí)行的轉(zhuǎn)移為(2,1,+A)，但C2中無(wú)消息A，因此Sender等待。處于狀態(tài)2的Receiver檢測(cè)到C1中存在消息R，滿足轉(zhuǎn)移(1,2,+R)激活條件，Receiver接收R(從C1中將R取走)，當(dāng)前狀態(tài)變?yōu)?。C1C2+ASender21-R+R-AReceiver21RC1C2+ASender21-R+R-AReceiver215.2.1CFSM此時(shí)Sender處于狀態(tài)2，可執(zhí)行的轉(zhuǎn)移為(2,1,+A)，但C2中無(wú)消息A，因此Sender等待。處于狀態(tài)2的Receiver執(zhí)行輸出轉(zhuǎn)移(1,2,-A)，將A放入通道C2，當(dāng)前狀態(tài)回到1。C1C2+ASender21-R+R-AReceiver21C1C2+ASender21-R+R-AReceiver21A5.2.1CFSM此時(shí)Receiver處于狀態(tài)1，可執(zhí)行的轉(zhuǎn)移為(1,2,+R)，但C1中無(wú)消息R，因此Receiver等待。處于狀態(tài)2的Sender檢測(cè)到C2中存在消息A，滿足轉(zhuǎn)移(2,1,+A)激活條件，Sender接收A(從C2中將A取走)，當(dāng)前狀態(tài)變?yōu)?。C1C2+ASender21-R+R-AReceiver21AC1C2+ASender21-R+R-AReceiver215.2.1CFSM若輸入通道為空，接收狀態(tài)無(wú)法執(zhí)行接收轉(zhuǎn)移。當(dāng)Sender和Receiver均處于接收狀態(tài)，并且通道為空，則協(xié)議無(wú)法繼續(xù)運(yùn)行，該狀態(tài)稱為死鎖，如上圖所示。C1C2+ASender21-R+R-AReceiver215.2.1CFSM若通道C2中存在消息B，而Sender無(wú)法執(zhí)行接收轉(zhuǎn)移(2,1,+B)。則協(xié)議無(wú)法繼續(xù)運(yùn)行，該狀態(tài)稱為意外輸入，如上圖所示。C1C2+ASender21-R+R-AReceiver21B5.2.1CFSMReceiver的狀態(tài)3永遠(yuǎn)無(wú)法成為當(dāng)前狀態(tài)，該狀態(tài)稱為不可執(zhí)行狀態(tài)。轉(zhuǎn)移(2,3,+B)和(3,1,-C)永遠(yuǎn)不會(huì)被執(zhí)行，這種轉(zhuǎn)移被稱為不可執(zhí)行轉(zhuǎn)移。C1C2+ASender21-R+R-AReceiver21B3-C+B5.2.1CFSM5.2.1CFSM協(xié)議狀態(tài)用狀態(tài)矩陣表示為：這里，E1,E2,…,En為幾個(gè)協(xié)議實(shí)體的局部狀態(tài)，Cij為協(xié)議實(shí)體i到協(xié)議實(shí)體j的通道的狀態(tài)。當(dāng)所有通道可處理成空通道時(shí)，協(xié)議狀態(tài)可用數(shù)組[E1,E2,…,En]表示?！F盡(exhausive)可達(dá)性分析產(chǎn)生和檢查所有協(xié)議狀態(tài)。以下算法描述窮盡可達(dá)性分析的基本思路：

start(){W={initialstate};A={};analyze();}analyze(){if(W==empty)return;q=elementfromW;addqtoA;findallsuccessorsofq;if(q==error_state)report_error();else{foreachsuccessorstatesofqif(sisnotinAorW){addstoW;analyze();}deleteqfromW;}}5.2.2窮盡可達(dá)性分析集合W包含未被分析的協(xié)議狀態(tài)，A包含已分析和正在分析中的協(xié)議狀態(tài)。算法執(zhí)行之前，W包含initialstate，A為空，算法執(zhí)行完畢之后，W為空，A包含協(xié)議的所有可達(dá)狀態(tài)。該算法假定計(jì)算機(jī)的存貯空間足夠大，計(jì)算速度足夠高。5.2.2窮盡可達(dá)性分析5.2.2窮盡可達(dá)性分析5.2.2窮盡可達(dá)性分析不考慮報(bào)文順序號(hào)，AB協(xié)議系統(tǒng)如圖所示，其中C12是S到R的通道，C21是R到S的通道，協(xié)議狀態(tài)由二維矩陣組成。初始狀態(tài)有四個(gè)后繼狀態(tài)：

……狀態(tài)（1）

……狀態(tài)（2）

……狀態(tài)（3）

……狀態(tài)（4）5.2.2窮盡可達(dá)性分析顯然，狀態(tài)(2)，(3)和(4)不是可達(dá)狀態(tài)。如何判定(1)是可達(dá)狀態(tài)，而(2)，(3)和(4)不是可達(dá)狀態(tài)。按下述格式定義交互事件：

entity(state):action-point(state)?/!message

entity(state)表示協(xié)議實(shí)體處于狀態(tài)state中，action-point(state)表示作用點(diǎn)處于狀態(tài)state中，!表示發(fā)送，?表示接收。作用點(diǎn)的狀態(tài)定義為“0”或“1”，發(fā)送(!)結(jié)束后，狀態(tài)為“1”，接收(?)結(jié)束后，狀態(tài)為“0”。AB協(xié)議系統(tǒng)有四個(gè)作用點(diǎn)，它們是用戶和S之間接口A，用戶和R之間接口B，S和通道之間接口a和R和通道之間接口b。利用上述的事件表達(dá)格式，上頁(yè)圖對(duì)應(yīng)的事件表述如下：5.2.2窮盡可達(dá)性分析事件(1)S(0):A(1)?m事件(8)R(1):B(0)!m事件(2)S(1):a(0)!m事件(9)C12(0):a(1)?m事件(3)S(2):timeout事件10)C12(1):drop事件(4)S(2):a(1)?ack事件(11)C12(1):b(0)!m事件(5)R(0):b(1)?m事件(12)C21(0):b(1)?ack事件(6)R(1):drop事件(13)C21(1):a(0)!ack事件(7)R(1):b(0)!ack5.2.2窮盡可達(dá)性分析則狀態(tài)(1)，(2)，(3)和(4)分別對(duì)應(yīng)事件(1)，(9)，(5)和(12)。初始狀態(tài)時(shí)：

A=1,B=0,a=0,b=0因此事件(5)，(9)和(12)均不可執(zhí)行。可見利用作用點(diǎn)標(biāo)識(shí)，可以很容易判斷協(xié)議處于狀態(tài)q時(shí)，那些事件可以被執(zhí)行，因而可以找到相應(yīng)的后續(xù)狀態(tài)。5.2.2窮盡可達(dá)性分析事件(1)S(0):A(1)?m事件(8)R(1):B(0)!m事件(2)S(1):a(0)!m事件(9)C12(0):a(1)?m事件(3)S(2):timeout事件10)C12(1):drop事件(4)S(2):a(1)?ack事件(11)C12(1):b(0)!m事件(5)R(0):b(1)?m事件(12)C21(0):b(1)?ack事件(6)R(1):drop事件(13)C21(1):a(0)!ack事件(7)R(1):b(0)!ack5.2.2窮盡可達(dá)性分析去掉內(nèi)部作用狀態(tài)，而根據(jù)通道狀態(tài)來(lái)判定那些事件會(huì)被執(zhí)行，將使算法變得簡(jiǎn)潔。用這種方法時(shí)，外部作用點(diǎn)保留，通道內(nèi)的事件隱藏起來(lái)。AB協(xié)議系統(tǒng)的事件簡(jiǎn)化為：通道內(nèi)的事件無(wú)需表示出來(lái)，通道C12的drop事件迭加到事件（6）中。

事件(1)S(0):A(1)?m事件(5)R(0):C12(1)?m事件(2)S(1):C12(0)!m事件(6)R(1):drop事件(3)S(2):timeout事件(7)R(1):C21(0)!ack事件(4)S(2):C21(1)?ack事件(8)R(1):B(0)!m5.2.2窮盡可達(dá)性分析如果通道為隊(duì)列通道，它的狀態(tài)定義就會(huì)變得復(fù)雜，狀態(tài)數(shù)也會(huì)急劇增加，事件的表達(dá)方法也變得復(fù)雜。例如，對(duì)于邊界為n的隊(duì)列通道，事件表達(dá)形式可能為：

entity(state):channel(state<n)!message就是說(shuō)，當(dāng)通道隊(duì)列長(zhǎng)度小于n時(shí)，協(xié)議實(shí)體entity才會(huì)執(zhí)行報(bào)文發(fā)送事件。C1C2-R+ASender21+R-AReceiver21CFSMCFSM-Bgsn：全局狀態(tài)標(biāo)識(shí)11EE21RE-R21BEgs0gs2-B意外輸入，接收者無(wú)法確定如何處理消息B。E:通道空22EE+R21EA-A+Ags1gs3gs4可達(dá)圖例：根據(jù)初始狀態(tài)獲得所有可能的狀態(tài)。5.2.2窮盡可達(dá)性分析從全局初始態(tài)(所有通道為空，各實(shí)體均處于其初始態(tài))開始，嘗試執(zhí)行所有可能的轉(zhuǎn)移，遍歷所有可達(dá)的狀態(tài)。將死鎖和意外輸入的狀況用獨(dú)立的全局狀態(tài)標(biāo)識(shí)，仔細(xì)驗(yàn)證導(dǎo)致死鎖和意外輸入的原因，如果是協(xié)議本身的錯(cuò)誤，則修改協(xié)議；如果是協(xié)議實(shí)現(xiàn)的疏忽，則指定相應(yīng)的補(bǔ)救措施。通過(guò)檢測(cè)通道中的消息數(shù)量，設(shè)計(jì)協(xié)議所需的緩沖區(qū)空間。通過(guò)標(biāo)注可達(dá)的狀態(tài)和已執(zhí)行的轉(zhuǎn)移，發(fā)現(xiàn)不可達(dá)狀態(tài)和不可執(zhí)行轉(zhuǎn)移。5.2.2窮盡可達(dá)性分析對(duì)(M,N)構(gòu)成的CFSM模型實(shí)施可達(dá)性分析。如果通道為FIFO類型，則驗(yàn)證需要多大的緩沖區(qū)空間？檢驗(yàn)是否存在不可達(dá)狀態(tài)和不可執(zhí)行的轉(zhuǎn)移？5.2.2窮盡可達(dá)性分析隨著協(xié)議機(jī)制復(fù)雜性的提高和隊(duì)列通道邊界值的增大，狀態(tài)爆炸問題使窮盡可達(dá)性分析變得無(wú)法實(shí)行。

非窮盡可達(dá)性分析技術(shù)為解決這個(gè)問題提供可行的辦法。將窮盡可達(dá)性搜索算法的語(yǔ)句foreachsuccessorstatesofq改為forsomesuccessorstatesofq,其它語(yǔ)句不變，就得到非窮盡可達(dá)性分析算法。

5.2.3非窮盡可達(dá)性分析非窮盡可達(dá)性分析的關(guān)鍵問題是，怎樣從q的所有后繼狀態(tài)中選取某些狀態(tài)進(jìn)行分析。

被選取的狀態(tài)應(yīng)該最有價(jià)值，最有分析意義，能最大可能檢測(cè)協(xié)議錯(cuò)誤的狀態(tài)。5.2.3非窮盡可達(dá)性分析事件優(yōu)先選擇法協(xié)議實(shí)體優(yōu)先選擇法純粹隨機(jī)選擇法5.2.3非窮盡可達(dá)性分析事件優(yōu)先選擇法5.2.3非窮盡可達(dá)性分析

事件t1,t2,……,tn使?fàn)顟B(tài)q產(chǎn)生n個(gè)后繼狀態(tài)，如果給這些事件賦于一定優(yōu)先級(jí)，那么被選擇的后繼狀態(tài)（一般只選擇一個(gè)），應(yīng)該是優(yōu)先級(jí)別數(shù)高的事件產(chǎn)生的。優(yōu)先級(jí)別數(shù)值的賦值方法：事件優(yōu)先選擇法5.2.3非窮盡可達(dá)性分析靜態(tài)賦值?？蛇_(dá)性分析進(jìn)行之前，按照一定原則（發(fā)送事件優(yōu)先于接收事件，協(xié)同事件高于內(nèi)部事件，等等）對(duì)所有事件賦于靜態(tài)優(yōu)先數(shù)值，分析過(guò)程中，這些數(shù)值不改變。動(dòng)態(tài)賦值?？蛇_(dá)性分析執(zhí)行之前，所有事件賦于相同的優(yōu)先數(shù)值（也可以不同），可達(dá)性分析過(guò)程中，事件每執(zhí)行一次，其優(yōu)先數(shù)減1。這種方法可均衡各個(gè)事件的執(zhí)行次數(shù)，使本來(lái)很少有機(jī)會(huì)執(zhí)行的事件能盡快的執(zhí)行一次。協(xié)議實(shí)體優(yōu)先選擇法5.2.3非窮盡可達(dá)性分析如果事件t1,t2,……,tn是由多個(gè)不同協(xié)議實(shí)體執(zhí)行的，那么被選擇的后繼狀態(tài)應(yīng)該是優(yōu)先級(jí)別高的協(xié)議實(shí)體所執(zhí)行的事件產(chǎn)生的。協(xié)議實(shí)體的優(yōu)先級(jí)別的賦值方法：協(xié)議實(shí)體優(yōu)先選擇法5.2.3非窮盡可達(dá)性分析靜態(tài)賦值。按照一定原則（發(fā)方高于收方，響應(yīng)方高于發(fā)起方，等等）賦給各個(gè)協(xié)議實(shí)體優(yōu)先級(jí)別，可達(dá)性分析進(jìn)行過(guò)程，數(shù)值不改變。協(xié)議實(shí)體優(yōu)先選擇法5.2.3非窮盡可達(dá)性分析動(dòng)態(tài)賦值方法之一。按照?qǐng)?zhí)行事件的多少或最后一次執(zhí)行事件的時(shí)間動(dòng)態(tài)改變優(yōu)先數(shù)值。例如，事件執(zhí)行多的協(xié)議實(shí)體優(yōu)先級(jí)別數(shù)降低，很長(zhǎng)時(shí)間未執(zhí)行任何事件的協(xié)議實(shí)體的優(yōu)先級(jí)別數(shù)提高，等等。動(dòng)態(tài)賦值方法之二。按照事件的相關(guān)特性動(dòng)態(tài)調(diào)整優(yōu)先級(jí)別。例如當(dāng)協(xié)議實(shí)體A執(zhí)行完發(fā)送事件之后，那么執(zhí)行該事件的協(xié)同事件的協(xié)議實(shí)體的優(yōu)先數(shù)值就立即提高，等等。純粹隨機(jī)選擇法5.2.3非窮盡可達(dá)性分析從q的n個(gè)后繼狀態(tài)中任取一個(gè)進(jìn)行分析。由于從q的n個(gè)后繼狀態(tài)中選擇“最有分析價(jià)格”的狀態(tài)是一個(gè)不可判定的問題，因此純粹隨機(jī)選擇方法是一種簡(jiǎn)單實(shí)用的方法。非窮盡可達(dá)性分析往往要進(jìn)行多次（每次的狀態(tài)選擇方法不同）才能得到較滿意的結(jié)果。

5.2.4協(xié)議錯(cuò)誤檢測(cè)方法可達(dá)性分析可檢測(cè)死鎖、活鎖、不可達(dá)狀態(tài)、不可執(zhí)行事件和意外輸入等協(xié)議錯(cuò)誤。如果q無(wú)任何后繼狀態(tài)，那么q就是死鎖狀態(tài)。5.2.4協(xié)議錯(cuò)誤檢測(cè)方法可達(dá)性分析可檢測(cè)死鎖、活鎖、不可達(dá)狀態(tài)、不可執(zhí)行事件和意外輸入等協(xié)議錯(cuò)誤。在窮盡可達(dá)性分析中，如果一個(gè)事件未被執(zhí)行一次，那么該事件可判定為不可執(zhí)行事件。對(duì)于非窮盡可達(dá)性分析，算法在執(zhí)行一遍之后，如果某些事件未執(zhí)行一次，那么在第二遍執(zhí)行中應(yīng)將這些事件的優(yōu)先級(jí)別數(shù)值提高，只有當(dāng)非窮盡可達(dá)性分析進(jìn)行多次之后，才能判定那些事件為不可執(zhí)行事件。5.2.4協(xié)議錯(cuò)誤檢測(cè)方法可達(dá)性分析可檢測(cè)死鎖、活鎖、不可達(dá)狀態(tài)、不可執(zhí)行事件和意外輸入等協(xié)議錯(cuò)誤。如果某個(gè)協(xié)議實(shí)體在執(zhí)行輸入事件之后所獲取的報(bào)文不是它所期待的報(bào)文，那么這個(gè)事件為意外輸入事件。意外輸入反映協(xié)議的完備性不好，即協(xié)議沒有考慮異常報(bào)文的接收處理等問題。5.2.4協(xié)議錯(cuò)誤檢測(cè)方法活鎖的檢測(cè)較為復(fù)雜，首先要檢測(cè)循環(huán)，常用方法：1)斷點(diǎn)法算法執(zhí)行多遍，執(zhí)行第n遍算法時(shí)，將前面(n-1)次算法檢測(cè)到的循環(huán)斷開，以便檢測(cè)新的循環(huán)。對(duì)于下頁(yè)圖所示的系統(tǒng)，算法執(zhí)行第一遍時(shí)，由t1,t2和t3產(chǎn)生的循環(huán)都能檢測(cè)出來(lái)。執(zhí)行第二遍算法時(shí)斷開(3)－(4)的轉(zhuǎn)換，那么由t4產(chǎn)生的循環(huán)(1)(2)(8)(9)(4)(5)就檢測(cè)出來(lái)了（注意：第二次執(zhí)行算法時(shí)，搜索順序不同于第一次）。執(zhí)行第三次算法時(shí)再斷開(8)－(9)，那么由t6產(chǎn)生的循環(huán)(1)(2)(8)(11)(9)(4)(5)就檢測(cè)出來(lái)了。

5.2.4協(xié)議錯(cuò)誤檢測(cè)方法2)標(biāo)記法算法執(zhí)行時(shí)，每檢測(cè)到一個(gè)循環(huán)就給處于循環(huán)之中的狀態(tài)打上“標(biāo)記”。如果q的某個(gè)后繼狀態(tài)不在W中而在A中，并且它已打上標(biāo)記，還須作進(jìn)一步判定是否真正產(chǎn)生了新的循環(huán)。判定規(guī)則：如果q的后繼狀態(tài)s在A中，并且s已打上標(biāo)記，且該循環(huán)序列的任何一個(gè)狀態(tài)或幾個(gè)仍然在W中，那么新的循環(huán)產(chǎn)生。5.2.4協(xié)議錯(cuò)誤檢測(cè)方法2)標(biāo)記法上頁(yè)圖中，當(dāng)算法執(zhí)行到狀態(tài)(9)時(shí)，它的后繼狀態(tài)(4)在A中，并且已處于兩個(gè)循環(huán)之中，這表明新的循環(huán)可能存在。由t3產(chǎn)生的循環(huán)的序列(3)(4)(5)中沒有一個(gè)狀態(tài)還處于W中，因此這個(gè)循環(huán)序列的所有狀態(tài)不包括在新的循環(huán)之中。由t1產(chǎn)生的循環(huán)的序列(1)(2)(3)(4)(5)中，(1)和(2)仍然處于W中，因此新的循環(huán)序列存在，循環(huán)序列由(1)(2)(8)(9)(4)(5)組成。當(dāng)算法執(zhí)行到狀態(tài)(10)時(shí)，雖然它的后繼狀態(tài)(6)在A中，但由于(6)未處于任何其它循環(huán)之中，因此不存在新的循環(huán)。

5.2.4協(xié)議錯(cuò)誤檢測(cè)方法當(dāng)所有循環(huán)都已檢測(cè)出來(lái)之后，就可以判定那些循環(huán)是死循環(huán)。死循環(huán)的判定是一件更為復(fù)雜的問題。通常通過(guò)“進(jìn)展?fàn)顟B(tài)”(progressstate)的標(biāo)記來(lái)確定一個(gè)循環(huán)是否為死循環(huán)。如果循環(huán)序列之內(nèi)包含至少一個(gè)進(jìn)展?fàn)顟B(tài)，那么它就不是死循環(huán)。進(jìn)展?fàn)顟B(tài)的標(biāo)記在可達(dá)性分析進(jìn)行之前手工完成。例如發(fā)送→超時(shí)→再發(fā)送構(gòu)成一個(gè)循環(huán)，如果再發(fā)送之前判定發(fā)送次數(shù)是否超過(guò)給定數(shù)值（超過(guò)給定值就轉(zhuǎn)向錯(cuò)誤處理），那么再發(fā)送狀態(tài)就可以標(biāo)記為進(jìn)展?fàn)顟B(tài)。5.3不變性分析如果一個(gè)系統(tǒng)的某個(gè)性質(zhì)能用一個(gè)確定的邏輯表達(dá)式描述，并且恒為真（不隨系統(tǒng)的狀態(tài)變化或執(zhí)行序列而改變），那么這個(gè)性質(zhì)稱為系統(tǒng)的不變性質(zhì)，簡(jiǎn)稱系統(tǒng)不變性。協(xié)議不變性分析包括：第一是找出系統(tǒng)（協(xié)議）的不變性質(zhì)，形成嚴(yán)格定義的不變性表達(dá)式；第二是以某種方式執(zhí)行協(xié)議，驗(yàn)證不變性表達(dá)式是否恒為真。我們所說(shuō)的不變性分析指的是第二項(xiàng)工作。不變性分析可采用兩種途徑：第一是不變性證明系統(tǒng)（往往采用歸納法），第二是不變性監(jiān)測(cè)系統(tǒng)。我們介紹第一種方法。5.3不變性分析用歸納法證明一個(gè)數(shù)學(xué)公式時(shí)，證明分三步進(jìn)行：第一步證明x=0時(shí)公式是否成立；第二步，假設(shè)x=n時(shí)公式成立；第三步，證明x=n＋1時(shí)公式是否成立。類似的，協(xié)議不變性證明也包括三步。首先，驗(yàn)證協(xié)議處于初始狀態(tài)時(shí)不變性表達(dá)式是否成立；然后，假定協(xié)議在某狀態(tài)下不變性成立；最后，驗(yàn)證協(xié)議從這個(gè)狀態(tài)開始執(zhí)行所有相關(guān)事件過(guò)程中不變性是否保持成立。5.3不變性分析以窗口流控制為例說(shuō)明其證明過(guò)程。/teaching/rn/animations/gbn_sr/5.3不變性分析以窗口流控制為例說(shuō)明其證明過(guò)程?；瑒?dòng)窗口流控制是點(diǎn)對(duì)點(diǎn)通訊協(xié)議（傳輸層，數(shù)據(jù)鏈路層）所廣泛采用的一種流控制方法。

發(fā)送端維護(hù)兩個(gè)計(jì)數(shù)器LW和HWLW：第一個(gè)已發(fā)送未認(rèn)可報(bào)文的順序號(hào)HW：下一次發(fā)送報(bào)文時(shí)能賦于的順序號(hào)HW–LW<=window所有未認(rèn)可報(bào)文放入ACKQUE隊(duì)列中

如果收到一個(gè)認(rèn)可報(bào)文,發(fā)送端將已認(rèn)可的報(bào)文從ACKQUE隊(duì)列中擦出，改變LW。5.3不變性分析以窗口流控制為例說(shuō)明其證明過(guò)程。接收端維護(hù)一個(gè)計(jì)數(shù)器NS，NS

=下一個(gè)準(zhǔn)備接收?qǐng)?bào)文的順序號(hào)。

如果所接收的報(bào)文的順序號(hào)不等于NS之值，丟棄該報(bào)文。

假定報(bào)文順序號(hào)為自然數(shù)并可無(wú)限增大。

對(duì)于這樣一個(gè)窗口流控制，可得出3個(gè)不變性表達(dá)式：5.3不變性分析

HW–LW≤window （1）

LW≤seq(elementofACKQUE)≤HW （2）

LW≤NS≤HW （3）其中：window為窗口寬度的最大值函數(shù)seq()的返回值為報(bào)文的順序號(hào)式(1)規(guī)定未認(rèn)可報(bào)文的個(gè)數(shù)必須小于或等于window式(2)規(guī)定ACKQUE隊(duì)列中的所有報(bào)文的順序號(hào)應(yīng)在窗口范圍之內(nèi)式(3)規(guī)定接收端的NS總是在窗口之內(nèi)5.3不變性分析協(xié)議中相關(guān)的原子操作包括：SM:(Sendamessage)If(HW–LW<window){seq(msg)=HW;HW=HW+1;sendthemsg;putthemsgtoACKQUE; }RA:(Receiveanack)If((theackisOK)and(LW<=seq(ack)<=HW)){deleteallmsgsinACKQUEwithseq(msg)<seq(ack);LW=seq(ack);}RS:(Re-sendmessagesaftertimeout)sendallmessagesinACKQUE;5.3不變性分析協(xié)議中相關(guān)的原子操作包括：RM:(Receiveamessage)

If((themsgisOK)and(seq(msg)==NS)){deliverthemsgtotheuser;

SA;NS=NS+1;}SA:(Sendtheack)sendtheackwithseq(ack)=NS;TM:(Transmitamessageoverthechannel)themsgmaybelostordestroyed;TA:(Transmitanackoverthechannel)theackmaybelostordestroyed;5.3不變性分析不變性表達(dá)式（3）的證明如下：第一步：初始化后，HW＝0，LW＝0，NS＝0因此LW＝NS＝HW。第二步：假定協(xié)議在執(zhí)行到某個(gè)狀態(tài)時(shí)，HW＝j(luò)，LW=i,NS=k，并且i≤k≤j成立。驗(yàn)證發(fā)端協(xié)議實(shí)體發(fā)出一個(gè)新的報(bào)文之后，協(xié)議在執(zhí)行所有相關(guān)原子操作之后，式（３）是否成立。5.3不變性分析第三步：SM發(fā)出順序號(hào)為j的報(bào)文之后，HW=j+1,LW≤NS＜HW，式（３）成立；TM不改變HW、LW和NS之值；如果超時(shí)事件產(chǎn)生，重發(fā)報(bào)文，RS不修改HW、LW和NS；由于SM執(zhí)行之后HW=j+1，當(dāng)RM執(zhí)行之后，NS＝k+1，式（３）仍然成立。如果所接收的報(bào)文順序號(hào)有錯(cuò)，RM不修改NS，因此式（３）成立：SA不改變HW、LW和NS；TA不修改HW、LW和NS，TA發(fā)出的ACK報(bào)文的順序號(hào)為k到j(luò)之間任意數(shù)值，即seq(ack)=k…j；RA正確執(zhí)行之后LW＝NS＝seq(ack)=k…j，而HW仍然為j+1，因此式（３）成立。如果RA丟棄ack報(bào)文，HW、LW和NS不變。5.4基于FSM等價(jià)性分析“等價(jià)”意味著某種程序上的“相同”和“無(wú)差別”。如果兩個(gè)協(xié)議模型或協(xié)議規(guī)范是等價(jià)的，那么它們可以互相替換，如果一個(gè)是正確的，那么另一個(gè)也是正確的。等價(jià)性分析的目的是證明兩個(gè)協(xié)議的FSM圖是等價(jià)的，典型的情況是證明協(xié)議規(guī)范和它的服務(wù)規(guī)范一致性。5.4基于FSM等價(jià)性分析按等價(jià)的含義和等價(jià)的強(qiáng)弱，等價(jià)性分為：1、觀察等價(jià)（observationalequivalence）如果對(duì)兩個(gè)協(xié)議進(jìn)行狀態(tài)到狀態(tài)的互相模擬時(shí)所觀察到的協(xié)議行為沒有差別，這兩個(gè)協(xié)議是觀察等價(jià)的。2、測(cè)試等價(jià)（testequivalence）如果對(duì)兩個(gè)協(xié)議施加相同的測(cè)試序列所觀察到的協(xié)議行為沒有差別，那么這兩個(gè)協(xié)議是測(cè)試等價(jià)的。3、蹤跡等價(jià)（traceequivalence）如果兩個(gè)協(xié)議執(zhí)行的事件序列是相同的，那么它們是蹤跡等價(jià)的。4、實(shí)現(xiàn)等價(jià)（implementationequivalence）如果一個(gè)協(xié)議所做的每一件事情都能被第二個(gè)模仿（mimic），反之亦然，那么它們是實(shí)現(xiàn)等價(jià)的。5.4基于FSM等價(jià)性分析生活中有哪些等價(jià)關(guān)系？5.4基于FSM等價(jià)性分析基于FSM的觀察等價(jià)性分析

對(duì)于狀態(tài)轉(zhuǎn)換系統(tǒng)（S,i,E,T），定義S*S為狀態(tài)映射集合。例如，一個(gè)包括三個(gè)狀態(tài)S0，S1和S2的FSM，S*S包括九種映射：（S0，S0），（S1，S1），（S2，S2），（S0，S1），…（S2，S1）。

互擬關(guān)系：如果兩個(gè)狀態(tài)p∈S，q∈S能互相模擬，那么（p,q）為互擬關(guān)系（bisimulationrelation）?；M關(guān)系分強(qiáng)互擬關(guān)系（strongbisimulationrelation）和弱互擬關(guān)系（weakbisimulationrelation）。5.4基于FSM等價(jià)性分析強(qiáng)狀態(tài)互擬關(guān)系：狀態(tài)轉(zhuǎn)換系統(tǒng)（S,i,E,T）的兩個(gè)狀態(tài)p∈S，q∈S為強(qiáng)互擬關(guān)系的充分必要條件是：對(duì)所有e∈E，如果存在一個(gè)p'∈S,p→e→p'∈T，那么就一定存在一個(gè)q'∈S,q→e→q'∈T，并且(p',q')為強(qiáng)互擬關(guān)系；如果存在一個(gè)q'∈S,q→e→q'∈T，那么就一定存在一個(gè)p'∈S,p→e→p'∈T，并且(p',q')為強(qiáng)互擬關(guān)系。5.4基于FSM等價(jià)性分析弱狀態(tài)互擬關(guān)系：狀態(tài)轉(zhuǎn)換系統(tǒng)（S,i,E,T）的兩個(gè)狀態(tài)p∈S，q∈S為弱互擬關(guān)系的充分必要條件是：對(duì)所有e∈E，e≠I

如果存在一個(gè)p'∈S,p→e→p'∈T，那么就一定存在一個(gè)q'∈S,q→e→q'∈T，并且(p',q')為弱互擬關(guān)系；如果存在一個(gè)q'∈S,q→e→q'∈T，那么就一定存在一個(gè)p'∈S,p→e→p'∈T，并且(p',q')為弱互擬關(guān)系。5