【文章內(nèi)容簡介】 中應(yīng)將這些事件的優(yōu)先級別數(shù)值提高。只有當(dāng)非窮盡可達(dá)性分析進(jìn)行多次之后，才能判定那些事件為無意義事件． （ 4） 如果某個(gè)協(xié)議實(shí)體在執(zhí)行輸入事件之后所獲取的報(bào)文不是它所期待的報(bào)文，那么這個(gè)事件為非確定輸入事件．非確定輸入事件反映協(xié)議的完備性不好，即協(xié)議沒有考慮異常報(bào)文的接收處理問題。 第五章 協(xié)議驗(yàn)證技術(shù) （ 6）活鎖（死循環(huán)）的檢測是非常麻煩的事情． 活鎖的檢測首先是循環(huán)的檢測．在算法 5 . 1 和 5 . 2 中，如果q 的后繼狀態(tài)已在 W 和 A 中存在時(shí)，那么循環(huán)可能存在．采用深度優(yōu)先搜索方法時(shí)，循環(huán)容易檢測（這是深度優(yōu)先搜索的優(yōu)點(diǎn)之二）：如果 q 的后繼狀態(tài) s 已在 W 中，那么 s 到 q 的狀態(tài)序列（依次排列在 W 中）這是一個(gè)循環(huán)．作為一個(gè)案例分析．我們來檢測圖 5 . 3 的循環(huán)，圖中狀態(tài)編號(hào)表示深度優(yōu)先搜索過程中算法所訪問的狀態(tài)的先后次序．狀態(tài)（ 5 ）有三個(gè)后繼狀態(tài)（ 1 ）、（ 3 ) 和（ 6 ) . ( 6 ）不在 W 中，它不構(gòu)成循環(huán)．后繼狀態(tài)（ 3 ）在 W 中，事件 t3產(chǎn)生循環(huán)，循環(huán)序列為（ 3 ) ( 4 ) ( 5 ) ．后繼狀態(tài)（ 1 ）在 w 中， t1產(chǎn)生循環(huán)，循環(huán)序列為（ I ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) ．深度優(yōu)先搜索方法不但容易檢測循環(huán)，而且很容易得出循環(huán)序列． 第五章 協(xié)議驗(yàn)證技術(shù) 現(xiàn)在的問題是，上述方法能檢測出所有循環(huán)嗎？答案是否定的，例如，圖 5 . 3中 t4，t5 ， t6和 t7，產(chǎn)生的循環(huán)就檢測不出來．當(dāng)算法執(zhí)行到狀態(tài)（ 9 ）時(shí)， ( 9 ）的后繼狀態(tài)之一（ 4 ）已不在 W 中而是在 A 中．當(dāng)算法執(zhí)行到狀態(tài)（ 10 ）時(shí)， ( 10 ）的后繼狀態(tài)（ 6 ）也在 A 中．前者 t4產(chǎn)生循環(huán)，后者 t5不產(chǎn)生循環(huán)，這就說明，如果 q 的后繼狀態(tài)在 A 中，循環(huán)可能存在。 第五章 協(xié)議驗(yàn)證技術(shù) 當(dāng) q的后繼狀態(tài)在 A中時(shí)，判定它是否產(chǎn)生循環(huán)有兩種方法。 第五章 協(xié)議驗(yàn)證技術(shù) 斷點(diǎn)法 算法執(zhí)行多遍，執(zhí)行第 n遍算法時(shí)，將前面（ n1）次算法已檢測到的循環(huán)斷開，以便檢測新的循環(huán)。對于圖 ，算法執(zhí)行第一遍時(shí)，由 t1，t2和 t3產(chǎn)生的循環(huán)都能檢測出來。執(zhí)行第二遍算法的時(shí)斷開（ 3） → （ 4）的轉(zhuǎn)換，那么由 t4產(chǎn)生的循環(huán)（ 1）（ 2）（ 8）（ 9）（ 4）（ 5）就檢測出來了（注意：第二次算法執(zhí)行時(shí)，搜索順序不同于第一次）。執(zhí)行第三次算法時(shí)再斷開（ 8） → （ 9），那么由 t6產(chǎn)生的循環(huán)（ 1）（ 2）（ 8）（ 11）（ 9）（ 4）（ 5）就檢測出來了。 第五章 協(xié)議驗(yàn)證技術(shù) ?標(biāo)記法 ?算法執(zhí)行過程中，每檢測到一個(gè)循環(huán)就給處于循環(huán)之中的狀態(tài)打上 “ 標(biāo)記 ” ，表明它已處于某個(gè)循環(huán)之中。如果 q的某個(gè)后續(xù)狀態(tài)不在 W中而在 A中，并且它已處于某個(gè)循環(huán)之中，那么是否真正產(chǎn)生了新的循環(huán)，還必須做進(jìn)一步判定。判定規(guī)則是：如果 q的后繼狀態(tài) s在 A中，并且 s已處于某個(gè)循環(huán)之中而且該循環(huán)序列的任何一個(gè)狀態(tài)或幾個(gè)仍然在 W中，那么新的循環(huán)產(chǎn)生。圖 ，當(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中，因此系 ind循環(huán)序列存在，循環(huán)序列由（ 1）（ 2）（ 3）（ 4）（ 5）組成。當(dāng)算法執(zhí)行到狀態(tài)（ 10）時(shí)，雖然它的后繼狀態(tài)（ 6）在 A中，但由于（ 6）未處于任何其他循環(huán)之中，因此不存在新的循環(huán)。 第五章 協(xié)議驗(yàn)證技術(shù) 當(dāng)所有循環(huán)已經(jīng)檢測出來之后，我們就可以判定那么循環(huán)是死循環(huán)。死循環(huán)的判定是更為復(fù)雜的問題。一種方法是通過 “ 進(jìn)展?fàn)顟B(tài)（ progress state） ” 的標(biāo)記來確定一個(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)行之前由手工進(jìn)行。例如發(fā)送 → 超時(shí) → 再發(fā)送構(gòu)成一個(gè)循環(huán)，如果發(fā)送之前判定發(fā)送次數(shù)是否超過給定數(shù)值（超過給定值就轉(zhuǎn)向錯(cuò)誤處理），那么再發(fā)送狀態(tài)就可以標(biāo)記為進(jìn)展?fàn)顟B(tài)。 第五章 協(xié)議驗(yàn)證技術(shù) 167。 不變性分析 如果一個(gè)系統(tǒng)的某個(gè)性質(zhì)能用一個(gè)確定的邏輯表達(dá)式描述，并且恒為真（不隨系統(tǒng)的狀態(tài)變化或執(zhí)行序列而改變），那么這個(gè)性質(zhì)稱為系統(tǒng)的不變性質(zhì)，簡稱系統(tǒng)不變性。協(xié)議的不變性分析包括二個(gè)工作：第一是完全正確的找出系統(tǒng)（協(xié)議）的不變性質(zhì)。形成嚴(yán)格定義的不變性表達(dá)式；第二是以某種方式執(zhí)行協(xié)議，驗(yàn)證不變性表達(dá)式是否恒為真。我們所說的不變性分析指的是第二項(xiàng)工作。第一項(xiàng)工作由手工進(jìn)行，許多協(xié)議描述文本也包含了不變性表達(dá)式。 不變性分析可采用兩種途徑：第一是不變性證明系統(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í)公式是否成立。類似的，協(xié)議不變性證明也包括兩步。首先，驗(yàn)證協(xié)議處于初始狀態(tài)時(shí)不變性表達(dá)式是否成立，然后假設(shè)協(xié)議在某狀態(tài)下不變性成立，驗(yàn)證協(xié)議從這個(gè)狀態(tài)開始執(zhí)行所有相關(guān)過程中不變性是否保持成立。 我們以窗口流控制為例說明其證明過程，案例來自于文獻(xiàn)資料 【 10】 ，本文已作剪輯。 第五章 協(xié)議驗(yàn)證技術(shù) 滑動(dòng)窗口流控制是點(diǎn)對點(diǎn)通訊協(xié)議（傳輸層，數(shù)據(jù)鏈路層）所廣泛采用的一種流控制方法。發(fā)送端維持兩個(gè)計(jì)數(shù)器 LW和 HW， LW之值等于第一個(gè)未認(rèn)可報(bào)文的順序號(hào)， HW之值為下一次發(fā)送報(bào)文時(shí)能賦予的順序號(hào)，HW和 LW之間差為發(fā)送窗口，窗口寬度不應(yīng)大于給定值。所有為認(rèn)可報(bào)文放入 ACKQUE隊(duì)列中，如果收到一個(gè)認(rèn)可報(bào)文，發(fā)送端將已認(rèn)可的報(bào)文從 ACKQUE隊(duì)列中擦去，并修改 LW之值。接收端維持一個(gè)計(jì)數(shù)器 NS， NS之值為下一個(gè)接受報(bào)文的順序號(hào)。如果所接受的報(bào)文的順序號(hào)不等于 NS之值，丟棄該報(bào)文。假定報(bào)文順序號(hào)為自然數(shù)并可以無限增大，那么對于這樣一個(gè)窗口流控制，我們可形成 3個(gè)不變性表達(dá)式： HW — LW window LW seq(element of ACKQUE) HW LW NS HW 第五章 協(xié)議驗(yàn)證技術(shù) 這里， window為窗口寬度的最大值，函數(shù)seq()的返回值為報(bào)文的順序號(hào)。表達(dá)式 1規(guī)定為認(rèn)可報(bào)文的個(gè)數(shù)必須小于或等于 window，表達(dá)式 2規(guī)定 ACKQUE隊(duì)列中的所有報(bào)文的順序號(hào)應(yīng)在窗口范圍之內(nèi)，表達(dá)式 3規(guī)定接收端的 NS總是在窗口之內(nèi)。 第五章 協(xié)議驗(yàn)證技術(shù) ? 為了用歸納法證明上述窗口流控制的不變性，我們必須羅列出協(xié)議中的所有相關(guān)的原子操作。這些原子操作包括： ? SM:(Send a message) ? If( HW － LW window) ? { ? Seq(message) = HW。 ? HW = HW+1