協議驗證

對協議本身的邏輯正確性進行校驗的過程稱之為協議驗證（protocol verification）。

協議驗證有兩種途徑：

（1）協議分析（protocol analysis）

（2）協議綜合（protocol synthesis）

通常所説的協議驗證指的是前者。協議綜合將協議設計過程和協議驗證(分析)過程融合在一起，它通過一組能確保所設計的協議是正確的規則，從一些基本協議模塊中（這些基本模塊已證明是正確的）產生所希望的目標協議。

協議分析的目的是：對已設計的協議進行分析和校驗（這些已設計的協議大都是採用非形式化設計方法產生的 ）

協議分析包括許多方法，例如，

（1）可達性分析（reachability analysis）

（2）不變性分析（invariance analysis）

（3）等價性分析（equivalence analysis）

（4）符號執行（symbol execution）、模擬（simulation）等等。

這些分析工作可以手動完成。

協議有多種表達形式，這包括：用自然語言描述的非形式化協議文本；用形式描述語言（ESTELLE，LOTOS,SDL等）描述的協議規範；用協議模型技術（FSM，Petrinet，CCS等）表達的協議模型；以及用程序設計語言（C，Pascal等）描述的協議代碼。協議分析可在任何一種表達形式上進行，一般地説，上述所有方法都可在這幾種表達形式上進行（手工或軟件工具）。然而，除符號執行之外，人們都在協議模型上進行協議分析。

這裏介紹三種分析方法，它們是可達性分析、不變性分析和等價分析。 ^[1] 

可達性分析是最常用的協議驗證方法。它試圖產生和檢查協議所有或部分可達狀態。“可達狀態”是指協議從初始狀態開始經歷有限次轉換之後可達到的狀態。所有可達狀態構成可達圖(RG: Reachability Graph)。

可達性分析的原理是：採用窮舉法檢查同一層內兩個或多個協議實體間所有可能的交互所產生的狀態。將協作的協議實體的狀態以及連接這些協議實體的低層稱為系統的全局狀態或混合狀態(composite or global state)。從一個給定的初始狀態開始，所有可能的變遷(用户命令、超時、報文到達等)產生許多新的全局狀態。對每一個新產生的狀態重複執行上述過程直到沒有新的狀態產生(某些變遷將導致系統返回到已產生的狀態)。 對於一個給定的初始狀態和一組關於低層協議的假定(提供的服務的類型)，這種分析能夠確定協議可能產生的所有結果。

可達性分析最適合於用狀態變遷模型描述的協議模型。對於狀態變遷模型的全局狀態空間的產生也比較容易自動化，已有很多作此用途的工具。對於程序語言描述的協議模型也可以使用可達性分析方法。具體做法是：在程序中設置許多斷點(break points)，這些斷點有效地定義了系統的控制狀態。 ^[2] 

如果一個系統的某個性質能用一個確定的邏輯表達式描述，並且恆為真（不隨系統的狀態變化或執行序列而改變），那麼這個性質稱為系統的不變性質，簡稱系統不變性。協議的不變性分析包括二個工作：第一是完全正確地找出系統（協議）的不變性質。形成嚴格定義的不變性表達式；第二是以某種方式執行協議，驗證不變性表達式是否恆為真。我們所説的不變性分析指的是第二項工作。第一項工作由手工進行，許多協議描述文本也包含了不變性表達式。

不變性分析可採用兩種途徑：第一是不變性證明系統（往往採用歸納法），第二是不變性監測系統。下面分別介紹它們。 ^[2] 

採用歸納法時，協議不變性證明包括兩步：驗證協議處於初始狀態時不變性表達式是否成立； 然後，假定協議在某狀態下不變性成立，驗證協議從這個狀態開始執行所有相關事件過程中不變性是否保持成立。 ^[2] 

不變性監測系統藉助監測軟件和監測方法對模擬運行或符號執行中的協議進行不變性校驗的過程稱之為不變性監測(invariant monitoring)。這種方法要求在協議代碼中插入斷點(子程序的調用或返回可視為自然斷點)，每個斷點處，監測系統取相關變量值，計算並校驗不變性表達式是否成立。通過監測系統進行不變性分析時，還會遇到一個麻煩問題：協議系統由多個協議實體組成(分佈性)，監測系統必須凌駕於它們之上，實現起來比較困難。

不變性監測程序還可對程序斷言(assert)進行校驗，程序斷言是嵌於協議代碼指定地方的特殊語句，例如ASSERT(state = =1)。協議代碼運行到ASSERT語句時將指示監測程序對ASSERT語句所申明的布爾表達式進行校驗。不變性表達式則要求無論系統(協議)處於何種狀態，不變性表達式都必須成立。此外，不變性表達式不同於程序斷言之處還在於它無需插入協議代碼中。 ^[2] 

“等價”意味着某種程度上的“相同”和“無差別”。如果兩個協議模型或協議規範是等價的，那麼它們可以互相替換，如果一個是正確的，那麼另一個也是正確的。等價性分析的另一個途徑是證明兩個協議的FSM圖或CCS表達式是等價的，典型的情況是證明協議規範和它的服務規範一致性。 ^[2] 

等價性分類如下：

按等價的含義和等價的強弱，等價性分為：

觀察等價（observational equivalence）：如果對兩個協議進行狀態到狀態的互相模擬時所觀察到的協議行為沒有差別，這兩個協議是觀察等價的。

測試等價（test equivalence）：如果對兩個協議施加相同的測試序列所觀察到的協議行為沒有差別，那麼這兩個協議是測試等價的。

跟蹤等價（trace equivalence）：如果兩個協議執行的事件序列是相同的，那麼它們是蹤跡等價的。

實現等價（implementation equivalence）：如果一個協議所做的每一件事情都能被第二個模仿（mimic），反之亦然，那麼它們是實現等價的。

這四種等價按強弱程度排列的話，順序是：觀察等價、測試等價、跟蹤等價、實現等價，其中觀察等價還分為強觀察等價和弱觀察等價。等價性的強弱反映兩個協議對行為細節的相同程度，等價性越強，它們的行為細節的相同程度越高。 ^[2] 

協議驗證的最主要內容是檢查協議是否滿足規定的協議性質。一般情況下，將協議性質分為兩類：

一般性質(general properties)。指所有協議所具有的一些公共特性。不同文獻對這類性質的個數和描述也不盡相同。

特殊性質(specific properties)。是指與具體協議內容有關的性質。對這些性質的定義構成了服務規範的主體內容。 ^[1] 

可達性(Reachability)：驗證協議的各種可能狀態之間的可達關係。如果協議的某個狀態從初態不可達，則表明協議有錯誤。如果從狀態A到狀態B的變遷不可能發生(直接或間接)，則從狀態A到狀態B是不可達的。

沒有死鎖(Deadlock freeness)：最典型的死鎖是協議中各實體都處於這樣的一種等待狀態，即只有在“某一事件”發生後才能做進一步的動作，但在該狀態下，這個“某一事件”卻不可能發生。死鎖發生時，協議所處的狀態稱為死鎖狀態。

沒有活鎖(Livelock freeness) ：活鎖是指協議處於無限的死循環中，而沒有別的事件可使協議從這一循環中解脱出來。例如，協議無限制地執行超時重發操作，但總是收不到對方的確認信息。狀態還是在變化的，不過不能脱離這種死循環狀態而已。

弱活鎖(Weak livelock)：是指協議處於死循環中，只有當協議交換命令的相對速度達到某一狀態時，協議才退出死循環。

時間相關的活鎖(Time-dependent livelock)：也稱為臨時阻塞(Tempo-blocking)。它是指協議處於死循環中，但是當通信雙方交換報文的相對速度到達某一狀態時，協議可以從死循環中出來。

有界性(Boundedness)：檢驗協議的某些成分或參數的容量(例如：通道容量、窗口大小)是否有界。有界性是針對協議元素性質和通道性質而言。

可恢復性或自同步性（Recovery from failures）：這是當出現差錯後，協議能否在有限的步驟內返回到正常狀態(包括初始態)執行。

無狀態二義性(State ambiguities freeness)：一個進程在某一時刻只允許具有一個穩定狀態。所謂穩定狀態是指當通信雙方的通道為空時的進程狀態。若在某一時刻進程可以有多個穩定狀態，則稱該進程的狀態為二義狀態。

互斥性(Mutual exclusion)：互斥性是指有些協議動作不能同時被多個用户執行。例如，多個用户不能同時請求同一資源。

終止或進展(Termination or Progress)：是指協議提供的服務必須在有限時間內完成。終止是針對終止協議(terminating protocols)而言，意思是指協議總是能到達期望的結束狀態。而進展則是針對循環協議(cyclic protocols)而言，意思是指協議總是能到達它的初始狀態。

無冗餘描述(Absence of Overspecification)：協議規範中沒有無用的、冗餘描述，例如，沒有未經實踐的報文接收(absence of unexercised message receptions)。

公平性(Fairness)：是指每一個協議實體均應平等地得到運行的機會，無論其它的協議實體想做什麼。 ^[1] 

完整性(Completeness)。是指協議設計考慮了所有可能發生的事件、選項以及服務。檢驗協議是否能處理所有可能的輸入，即是否缺少應用的處理，或有無非期待的接收或輸入(即錯收)。

一致性(consistency)。是指協議服務行為(或性質)和協議行為(或性質)一致，即協議應該提供用户要求的服務，而無需提供用户沒有要求的服務。 ^[1]