【正文】 } 5 . 2 . 2 非窮盡可達(dá)性分析 將算法 5 . 1 的語句 for each successor state s of q 改為 for some successor state s of q, 其它語句不變，我們就得到非窮盡可達(dá)性分析算法 第五章 協(xié)議驗(yàn)證技術(shù) 現(xiàn)在問題是，怎樣從 q 的所有后繼狀態(tài)中選取某些（ some）狀態(tài)進(jìn)行分析，當(dāng)然，被選取的狀態(tài)應(yīng)該是最有價(jià)值的，最有分析意義的，能最大可能檢測協(xié)議錯(cuò)誤的狀態(tài)． 1 ．事件優(yōu)先選擇法 事件 t1,t2…… tn使?fàn)顟B(tài) q 產(chǎn)生 n 個(gè)后繼狀態(tài)（圖 5 . 2 ) ，如果給這些事件賦于一定優(yōu)先級別數(shù)值，那么被選擇的后繼狀態(tài)（一般只選擇一個(gè)），應(yīng)該是優(yōu)先級別數(shù)高的事件產(chǎn)生的．優(yōu)先級別數(shù)值的賦值方法可以是： (1) 靜態(tài)賦值 可達(dá)性分析進(jìn)行之前，按照一定原則（發(fā)送事件優(yōu)先于接收事件，協(xié)同事件高于內(nèi)部事件等等）對所有事件賦于靜態(tài)優(yōu)先數(shù)值，可達(dá)性分析過程中，這些數(shù)值不改變． (2) 動(dòng)態(tài)賦值 可達(dá)性分析執(zhí)行之前，所有事件賦于相同的優(yōu)先數(shù)值（也可以不同），可達(dá)性分析過程中，事件每執(zhí)行一次，其優(yōu)先數(shù)減 1 。 第五章 協(xié)議驗(yàn)證技術(shù) 2 ．協(xié)議實(shí)體優(yōu)先選擇法 如果事件 t1,t2…… tn是由多個(gè)不同協(xié)議實(shí)體執(zhí)行的，那么被選擇的后繼狀態(tài)應(yīng)該是優(yōu)先級別高的協(xié)議實(shí)體所執(zhí)行的事件產(chǎn)生的．協(xié)議實(shí)體的優(yōu)先級別的賦值方法可以是： (1) 靜態(tài)賦值 按照一定原則（發(fā)方高于收方，響應(yīng)方高于發(fā)起方， … ，等等）賦給各個(gè) 協(xié)議實(shí)體優(yōu)先數(shù)值，可達(dá)性分析進(jìn)行過程，數(shù)值不改變． (2) 動(dòng)態(tài)賦值 方法之一 按照執(zhí)行事件的多少或最后一次執(zhí)行事件的時(shí)間動(dòng)態(tài)改變協(xié)議實(shí)體的優(yōu)先數(shù)值．例如．事件執(zhí)行多的協(xié)議實(shí)體優(yōu)先級別數(shù)降低，很長時(shí)間未執(zhí)行任何事件的協(xié)議實(shí)體的優(yōu)先級別數(shù)提高等等． 動(dòng)態(tài)斌值方法之二 按照事件的相關(guān)特性動(dòng)態(tài)調(diào)整協(xié)議實(shí)體的優(yōu)先級別數(shù)值．例如當(dāng)協(xié)議實(shí)體 A 執(zhí)行完發(fā)送事件之后，那么執(zhí)行該事件的協(xié)同事件的協(xié)議實(shí)體的優(yōu)先數(shù)值就立即提高等等． 第五章 協(xié)議驗(yàn)證技術(shù) 3 ．純粹隨機(jī)選擇法 這是最簡單而有效的選擇方法：從 q的 n 個(gè)后繼狀態(tài)中任取 1個(gè)或幾個(gè)進(jìn)行分析．由于從 q 的 n 個(gè)后繼狀態(tài)中選擇 “ 最有分析價(jià)值 ” 的狀態(tài)是一個(gè)不可判定的問題，因此純悴隨機(jī)選擇方法是一種簡單適用的方法。只有當(dāng)非窮盡可達(dá)性分析進(jìn)行多次之后，才能判定那些事件為無意義事件． （ 4） 如果某個(gè)協(xié)議實(shí)體在執(zhí)行輸入事件之后所獲取的報(bào)文不是它所期待的報(bào)文，那么這個(gè)事件為非確定輸入事件．非確定輸入事件反映協(xié)議的完備性不好，即協(xié)議沒有考慮異常報(bào)文的接收處理問題。 第五章 協(xié)議驗(yàn)證技術(shù) 當(dāng) q的后繼狀態(tài)在 A中時(shí)，判定它是否產(chǎn)生循環(huán)有兩種方法。對于圖 ，算法執(zhí)行第一遍時(shí)，由 t1，t2和 t3產(chǎn)生的循環(huán)都能檢測出來。執(zhí)行第三次算法時(shí)再斷開（ 8） → （ 9），那么由 t6產(chǎn)生的循環(huán)（ 1）（ 2）（ 8）（ 11）（ 9）（ 4）（ 5）就檢測出來了。如果 q的某個(gè)后續(xù)狀態(tài)不在 W中而在 A中，并且它已處于某個(gè)循環(huán)之中，那么是否真正產(chǎn)生了新的循環(huán)，還必須做進(jìn)一步判定。圖 ，當(dāng)算法執(zhí)行但狀態(tài)（ 9）時(shí)，它的后繼狀態(tài)（ 4）在 A中，并且已處于兩個(gè)循環(huán)之中，這表明新的循環(huán)可能存在。由 t1產(chǎn)生的循環(huán)序列（ 1）（ 2）（ 3）（ 4）（ 5）中，（ 1）和（ 2）仍然處于 W中，因此系 ind循環(huán)序列存在，循環(huán)序列由（ 1）（ 2）（ 3）（ 4）（ 5）組成。 第五章 協(xié)議驗(yàn)證技術(shù) 當(dāng)所有循環(huán)已經(jīng)檢測出來之后，我們就可以判定那么循環(huán)是死循環(huán)。一種方法是通過 “ 進(jìn)展?fàn)顟B(tài)（ progress state） ” 的標(biāo)記來確定一個(gè)循環(huán)是否為死循環(huán)。進(jìn)展?fàn)顟B(tài)的標(biāo)記在可達(dá)性分析進(jìn)行之前由手工進(jìn)行。 第五章 協(xié)議驗(yàn)證技術(shù) 167。協(xié)議的不變性分析包括二個(gè)工作：第一是完全正確的找出系統(tǒng)（協(xié)議）的不變性質(zhì)。我們所說的不變性分析指的是第二項(xiàng)工作。 不變性分析可采用兩種途徑：第一是不變性證明系統(tǒng)（往往采用歸納法），第二是不變性監(jiān)測系統(tǒng)。 第五章 協(xié)議驗(yàn)證技術(shù) 不變性證明系統(tǒng) 用歸納法證明一個(gè)數(shù)學(xué)公式時(shí)，證明分兩步進(jìn)行：第一步證明 x=0時(shí)公式是否成立；第二步，如果 x=n時(shí)公式成立，那么證明 x=n+1時(shí)公式是否成立。首先，驗(yàn)證協(xié)議處于初始狀態(tài)時(shí)不變性表達(dá)式是否成立，然后假設(shè)協(xié)議在某狀態(tài)下不變性成立，驗(yàn)證協(xié)議從這個(gè)狀態(tài)開始執(zhí)行所有相關(guān)過程中不變性是否保持成立。 第五章 協(xié)議驗(yàn)證技術(shù) 滑動(dòng)窗口流控制是點(diǎn)對點(diǎn)通訊協(xié)議（傳輸層，數(shù)據(jù)鏈路層）所廣泛采用的一種流控制方法。所有為認(rèn)可報(bào)文放入 ACKQUE隊(duì)列中，如果收到一個(gè)認(rèn)可報(bào)文，發(fā)送端將已認(rèn)可的報(bào)文從 ACKQUE隊(duì)列中擦去，并修改 LW之值。如果所接受的報(bào)文的順序號不等于 NS之值，丟棄該報(bào)文。表達(dá)式 1規(guī)定為認(rèn)可報(bào)文的個(gè)數(shù)必須小于或等于 window，表達(dá)式 2規(guī)定 ACKQUE隊(duì)列中的所有報(bào)文的順序號應(yīng)在窗口范圍之內(nèi)，表達(dá)式 3規(guī)定接收端的 NS總是在窗口之內(nèi)。這些原子操作包括： ? SM:(Send a message) ? If( HW － LW window) ? { ? Seq(message) = HW。 ? send the message。 ? } ? RA:(Receive an ack) ? { ? if (( the ack is OK) and (LW = seq(ack) =HW)) ? delete all message in ACKQUE with seq(message) seq(ack)。 ? } ? RS:(RE— send message after timeout) ? Send all message in ACKQUE。 ? NS = NS + 1。 ? TM:(Transmit a message over the channel) ? the message may be lost or destroyed。 第五章 協(xié)議驗(yàn)證技術(shù) 原子操作 SM， RA和 RS由發(fā)端協(xié)議實(shí)體執(zhí)行， RM和 SA由收端協(xié)議實(shí)體執(zhí)行， TM和 TA由通道執(zhí)行。下面用歸納法證明不變性 3。 第二步 假定協(xié)議在執(zhí)行到某個(gè)狀態(tài)時(shí) HW=j， LW=i， NS=k，并且 ikj成立。 SM SM發(fā)出順序號為 j的報(bào)文之后， HW= j+1， LWNSHW,表達(dá)式3成立 TM TM不改變 HW， LW和 NS的值； 第五章 協(xié)議驗(yàn)證技術(shù) RS 如果超時(shí)事件產(chǎn)生，重發(fā)報(bào)文， RS不修改 HW,LW和NS； RM 由于 SM執(zhí)行之后 HW=j+1，當(dāng) RM執(zhí)行之后，雖然NS=K+1，但表達(dá)式 3仍然成立。如果 RA丟棄 ack報(bào)文， HW,LW和 NS不變。 第五章 協(xié)議驗(yàn)證技術(shù) ? 不變性監(jiān)測系統(tǒng) ? 不變性監(jiān)測系統(tǒng)借助監(jiān)測軟件和監(jiān)測方法對模擬運(yùn)行或符號執(zhí)行中的協(xié)議進(jìn)行不變性校驗(yàn)的