• 作者： 粘添壽; 黃廣志
• 作者服務機構： 中山大學電機工程研究所; 高雄工商專科電機科
• 中文摘要： 本篇論文依協定的驗證及組合技術（Protocol Validation and Combination, PVC）發展一個可驗證Estelle所描述的通信協定。兩個主要技術被發展出來：(1)實體內技術是被用來驗證某個通信實體內的訊息傳遞，並且找出邏輯上的屬性。(2)實體間技術是被用來驗證兩個通信實體間的訊息傳遞。PVC可將一個Estelle所描述的通信協定依其通信模組，以數個定限狀態機械表示，因此我們可觀察到整個通信實體內和實體間的通信行為。
• 英文摘要： In this paper, we develop a validation technique for communication protocols specified by Estelle,based on the Protocol Validation and Combination (PVC) techniques. Two major approaches are developed:(1) the intra-entity approach is used to validate the communications in a communication entity to findtheir logical properties; (2) the inter-entity approach is used to validate the communications between twoentities．A communication protocol can be represented by several finite state machines, which dependon the communication modules, and we can then view and validate the whole communication intra-entityand inter-entity behavior of this protocol described by the Estelle formal specification.
• 中文關鍵字： communication protocol;Estelle; finite state machine; protocol validation; protocol combination; formal description tecinique
• 英文關鍵字： --