【正文】 a ? m12Cb ! md r o paBd r o pR01b!ack,B!mb?m第五章 協(xié)議驗證技術 為了解決這個問題，我們按下述格式定義交互事件： entity(state):action—point(state)?/!message 這里， entity(state)表示協(xié)議實體處于狀態(tài) state中，action —point(state)表示作用點處于狀態(tài) state中，！表示發(fā)送，？表示接收。 1 1 2 122 1 212nnnnnCCECCECC E????????第五章 協(xié)議驗證技術 不考慮報文順序號， AB協(xié)議系統(tǒng)如圖 ，其中是 R到S的通道，協(xié)議狀態(tài)由二維矩陣組成。 第五章 協(xié)議驗證技術 協(xié)議狀態(tài)用狀態(tài)矩陣表示為 : 這里 E1， E2… ， En，為 n層協(xié)議的幾個協(xié)議實體的局部狀態(tài)， Cij為協(xié)議實體 i到協(xié)議實體 j的通道的狀態(tài)。 } } 集合 W包含未被分析的協(xié)議狀態(tài)， A包含已分析和正在分析中的協(xié)議狀態(tài) , 算法執(zhí)行之前， W包含 initial state,A為空，算法執(zhí)行完畢之后 ,W為空， A包含協(xié)議的所有可達狀態(tài)。 analyze()。 if (q==error_state) report_error()。 add q to A。//窮盡分析 } analyze() { if (W==empty) return。//工作集；將被分析的狀態(tài) A={}。算法 的基本算法，該算法假定計算機的存儲空間足夠大，計算速度足夠高。可達性分析涉及三個重要技術： （ 1）怎樣找到所有可達狀態(tài)，構成可達圖； （ 2）怎樣檢測死鎖、活鎖等協(xié)議錯誤； （ 3）怎樣解決狀態(tài)爆炸問題。 第五章 協(xié)議驗證技術 可達性分析 可達性分析（基于 FSM模型技術）試圖產生和檢查協(xié)議所有或部分可達狀態(tài)。然而，除符號執(zhí)行之外，人們都在協(xié)議模型上進行協(xié)議分析（簡單，容易形成確定算法）。 協(xié)議有多種表達形式，這包括：用自然語言描述的非形式化協(xié)議文本；用形式描述語言（ ESTELLE,LOTOS,SDL等）描述的協(xié)議規(guī)范；用協(xié)議模型技術（ FSM， petri,CCS等）表達的協(xié)議模型；以及用程序設計語言（ C，pascal等）描述的協(xié)議代碼。 協(xié)議分析的目的是：對已設計的協(xié)議進行分析和校驗（這些已設計的協(xié)議大都是采用非形式化設計方法產生的 ） 第五章 協(xié)議驗證技術 協(xié)議分析包括許多方法，例如， （ 1） 可達性分析 （ reachability analysis） （ 2） 等價性分析 （ equivalence analysis） （ 3） 不變性分析 （ invariance analysis） （ 4）符號執(zhí)行（ symbol executin）、模擬（ simulation）等等。第五章 協(xié)議驗證（分析）技術 概述 對協(xié)議本身的邏輯正確性進行校驗的過程稱之為驗證（ protocol verification） . 協(xié)議驗證有兩種途徑： （ 1）協(xié)議分析（ protocol analysis） （ 2）協(xié)議綜合（ protocol synthesis） 通常所說的協(xié)議驗證指的是前者。協(xié)議綜合（將在第六章討論）將協(xié)議設計過程和協(xié)議驗證 (分析 )過程融合在一起，它通過一組能確保所設計的協(xié)議是正確的規(guī)則，從一些基本協(xié)議模塊中（這些基本模塊已證明是正確的）產生所希望的目標協(xié)議。 這些分析工作可以手動完成。協(xié)議分析可在任何一種表達形式上進行，一般地說，上述所有方法都可在這幾種表達形式上進行（手工或軟件工具）。 本章討論三種分析方法，它們是 可達性分析、不變性分析和等價分析 。所謂可達狀態(tài)指協(xié)議從初始狀態(tài)開始經歷有限次轉換之后可達到的狀態(tài)，所有可達狀態(tài)構成可達圖（ reachability graph） .可達性分析的最重要工作是產生和檢查可達圖，判定是否存在死鎖，活鎖等協(xié)議錯誤。 第五章 協(xié)議驗證技術 窮盡可達性分析 窮盡（ exnausive）可達性分析產生和檢查所有協(xié)議狀態(tài)。 第五章 協(xié)議驗證技術 算法 ： exhausive reachability analysis start() { W={initial state}。//被分析過的狀態(tài) analyze()。 q=last element from W。 find all successsors of q。 else { for each successor state s of q if (s is not in A or W) { add s to W。 } delete q from W。該算法簡單明了，然而要將它付諸實施時 ,我們還必須解決以下一些問題。當所有通道可處理成空通道時，協(xié)議狀態(tài)可用數(shù)組[E1,E2,… ,En]表示（因為空通道只有一種狀態(tài)）。初始狀態(tài)有四個后繼狀態(tài)： 0000??????A ? m1000??????( 1 )a ? m01( 2 )00??????b ? m01??????( 3 )b ? a c k0010( 4 )很顯然，狀態(tài)（ 2），（ 3）和（ 4）不是可達狀態(tài)(因為初始狀態(tài)中 AB內部沒有任何數(shù)據(jù)需要傳輸，所以（ 2），（ 3),(4)狀態(tài)是不可能出現(xiàn)的，即不可達的 )。作用點的狀態(tài)定義為 “ 0”或“ 1”。 AB協(xié)議系統(tǒng)有四個作用點，它們是用戶和 S之間接口 A，用戶和 R之間接口 B， S和通道之間接口 a以及 R和通道之間接口 b。例如，對于邊界為 n 的隊列通道，事件表述形式可能為： entity(state):channel(staten)!message. 就是說，當通道隊列長度小于 n 時，協(xié)議實體 entity 才會執(zhí)行報文發(fā)送事件。假定每個狀態(tài)有兩個后繼狀態(tài)，算法執(zhí)行 m 步之后，對于深度優(yōu)先搜索方法， W 的長度為 m ，但對于寬度優(yōu)先搜索， W 的長度為 2m。 5 . 2 . 3 討論各種協(xié)議錯誤的檢側方法。 A={}。 } analyse() { If (W==empty) return。 add q to A。 if (q == error_state) report_error()。 } Delete q from W }