Abstract
在通訊協定（Communicetino Protocols ）的規格表示與驗證（Speeificetion audVenfication）兩方面，一種稱為混合式的方法（Hubnid approach）巳被廣泛採用。在這論文裡面，一個由有限狀態轉換圖（Finite-State transation ）和邏輯語言（Pvolog Clcuses）結合而成的模式將被提出做詳盡的討論。我們利用有限狀態轉換技術，其狀態產生的可達性分析（Reachabilitg aualysis ）能容易的做機械化處理，同時過程中能自動的檢查出通訊協定本身可能發生的格式性質（Syutactie Pvopertrse）錯誤，諸如狀態死結（State Deadlock）無設定之接收運作（Llnspecified Reception）無執行可能的交互運作（Nonexecntable luteraction）和循環作用（Looping）等皆是。另外使用邏輯語言的最大好處即是它能將有關的轉換過程、程式變數、起動敘述、和運作描述等容易的表示成對應的斷言（Assertris ）或公理（Axioms）。而且在通訊協定的規格與其所提供的服務兩者間的一致性（Consisteuay ）也能在可達性分析的自動化過程中被推論證明出來，祗需設計有將所要證實的目標描述成一些特別的公理或目的（Goals ）的邏輯語言表示之。