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