協定驗證是指根據協定規範來檢查協定實體間的互動是否滿足一定特性(properties)或條件(conditions)的過程，例如，檢查是否有死鎖存在。通過協定驗證，可以獲知協定設計是否滿足正確性、完整性和一致性等要求。
基本介紹
- 中文名：協定驗證
- 外文名：protocol verification
- 目的：對協定進行分析和校驗
- 途徑：協定分析和協定綜合
- 工具：算法語言
- 領域：協定工程
概述,可達性分析,不變性分析,不變性證明系統,不變性監測系統,等價性分析,協定性質,一般性質,特殊性質,
概述
對協定本身的邏輯正確性進行校驗的過程稱之為協定驗證（protocol verification）。
協定驗證有兩種途徑：
（1）協定分析（protocol analysis）
（2）協定綜合（protocol synthesis）
（1）協定分析（protocol analysis）
（2）協定綜合（protocol synthesis）
通常所說的協定驗證指的是前者。協定綜合將協定設計過程和協定驗證(分析)過程融合在一起，它通過一組能確保所設計的協定是正確的規則，從一些基本協定模組中（這些基本模組已證明是正確的）產生所希望的目標協定。
協定分析的目的是：對已設計的協定進行分析和校驗（這些已設計的協定大都是採用非形式化設計方法產生的 ）
協定分析包括許多方法，例如，
（1）可達性分析（reachability analysis）
（2）不變性分析（invariance analysis）
（3）等價性分析（equivalence analysis）
（4）符號執行（symbol execution）、模擬（simulation）等等。
這些分析工作可以手動完成。
（1）可達性分析（reachability analysis）
（2）不變性分析（invariance analysis）
（3）等價性分析（equivalence analysis）
（4）符號執行（symbol execution）、模擬（simulation）等等。
這些分析工作可以手動完成。
協定有多種表達形式，這包括：用自然語言描述的非形式化協定文本；用形式描述語言（ESTELLE，LOTOS,SDL等）描述的協定規範；用協定模型技術（FSM，Petrinet，CCS等）表達的協定模型；以及用程式設計語言（C，Pascal等）描述的協定代碼。協定分析可在任何一種表達形式上進行，一般地說，上述所有方法都可在這幾種表達形式上進行（手工或軟體工具）。然而，除符號執行之外，人們都在協定模型上進行協定分析。
這裡介紹三種分析方法，它們是可達性分析、不變性分析和等價分析。
可達性分析
可達性分析是最常用的協定驗證方法。它試圖產生和檢查協定所有或部分可達狀態。“可達狀態”是指協定從初始狀態開始經歷有限次轉換之後可達到的狀態。所有可達狀態構成可達圖(RG: Reachability Graph)。
可達性分析的原理是：採用窮舉法檢查同一層內兩個或多個協定實體間所有可能的互動所產生的狀態。將協作的協定實體的狀態以及連線這些協定實體的低層稱為系統的全局狀態或混合狀態(composite or global state)。從一個給定的初始狀態開始，所有可能的變遷(用戶命令、逾時、報文到達等)產生許多新的全局狀態。對每一個新產生的狀態重複執行上述過程直到沒有新的狀態產生(某些變遷將導致系統返回到已產生的狀態)。 對於一個給定的初始狀態和一組關於低層協定的假定(提供的服務的類型)，這種分析能夠確定協定可能產生的所有結果。
可達性分析最適合於用狀態變遷模型描述的協定模型。對於狀態變遷模型的全局狀態空間的產生也比較容易自動化，目前已有很多作此用途的工具。對於程式語言描述的協定模型也可以使用可達性分析方法。具體做法是：在程式中設定許多斷點(break points)，這些斷點有效地定義了系統的控制狀態。
不變性分析
不變性分析可採用兩種途徑：第一是不變性證明系統（往往採用歸納法），第二是不變性監測系統。下面分別介紹它們。
不變性證明系統
採用歸納法時，協定不變性證明包括兩步：驗證協定處於初始狀態時不變性表達式是否成立； 然後，假定協定在某狀態下不變性成立，驗證協定從這個狀態開始執行所有相關事件過程中不變性是否保持成立。
不變性監測系統
不變性監測系統藉助監測軟體和監測方法對模擬運行或符號執行中的協定進行不變性校驗的過程稱之為不變性監測(invariant monitoring)。這種方法要求在協定代碼中插入斷點(子程式的調用或返回可視為自然斷點)，每個斷點處，監測系統取相關變數值，計算並校驗不變性表達式是否成立。通過監測系統進行不變性分析時，還會遇到一個麻煩問題：協定系統由多個協定實體組成(分布性)，監測系統必須凌駕於它們之上，實現起來比較困難。
不變性監測程式還可對程式斷言(assert)進行校驗，程式斷言是嵌於協定代碼指定地方的特殊語句，例如ASSERT(state = =1)。協定代碼運行到ASSERT語句時將指示監測程式對ASSERT語句所申明的布爾表達式進行校驗。不變性表達式則要求無論系統(協定)處於何種狀態，不變性表達式都必須成立。此外，不變性表達式不同於程式斷言之處還在於它無需插入協定代碼中。
等價性分析
“等價”意味著某種程度上的“相同”和“無差別”。如果兩個協定模型或協定規範是等價的，那么它們可以互相替換，如果一個是正確的，那么另一個也是正確的。等價性分析的另一個途徑是證明兩個協定的FSM圖或CCS表達式是等價的，典型的情況是證明協定規範和它的服務規範一致性。
等價性分類如下：
按等價的含義和等價的強弱，等價性分為：
觀察等價（observational equivalence）：如果對兩個協定進行狀態到狀態的互相模擬時所觀察到的協定行為沒有差別，這兩個協定是觀察等價的。
測試等價（test equivalence）：如果對兩個協定施加相同的測試序列所觀察到的協定行為沒有差別，那么這兩個協定是測試等價的。
跟蹤等價（trace equivalence）：如果兩個協定執行的事件序列是相同的，那么它們是蹤跡等價的。
實現等價（implementation equivalence）：如果一個協定所做的每一件事情都能被第二個模仿（mimic），反之亦然，那么它們是實現等價的。
這四種等價按強弱程度排列的話，順序是：觀察等價、測試等價、跟蹤等價、實現等價，其中觀察等價還分為強觀察等價和弱觀察等價。等價性的強弱反映兩個協定對行為細節的相同程度，等價性越強，它們的行為細節的相同程度越高。
協定性質
協定驗證的最主要內容是檢查協定是否滿足規定的協定性質。一般情況下，將協定性質分為兩類：
一般性質(general properties)。指所有協定所具有的一些公共特性。不同文獻對這類性質的個數和描述也不盡相同。
特殊性質(specific properties)。是指與具體協定內容有關的性質。對這些性質的定義構成了服務規範的主體內容。
一般性質
可達性(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)：是指每一個協定實體均應平等地得到運行的機會，無論其它的協定實體想做什麼。
特殊性質
完整性(Completeness)。是指協定設計考慮了所有可能發生的事件、選項以及服務。檢驗協定是否能處理所有可能的輸入，即是否缺少套用的處理，或有無非期待的接收或輸入(即錯收)。
一致性(consistency)。是指協定服務行為(或性質)和協定行為(或性質)一致，即協定應該提供用戶要求的服務，而無需提供用戶沒有要求的服務。
