• 作者： 黃崇明; 許政穆
• 作者服務機構： 國立成功大學資訊工程研究所電腦輔助設計協定工程實驗室
• 中文摘要： 在通信協定領域主，協定驗證主要目的是在偵測通信協定在設計階段是否有邏輯錯誤存在。在本論文中，我們提出一整合的協定驗證技術。首先我們提出一適用於ECFSM為協定描述之最大擴展協定驗證(maximal progress protocolverification），並且將此協定驗證加入漸進式的協定驗證方法。除此之外為了降低驗證過程中總體狀態的生成個數，我們亦整合了dead and live變數分析技術來減少總體狀態的生成數目。所以，我們所提出的漸進式最大擴展協定驗證，整合了數種的協定驗證技術所推導出來的。而在本論文中，我們所提出的以ECFSM為協定驗證方法可以直接應用於以同樣以ECFSM為基礎的正規描述技術(Formal Description Techniques, FDTs)，如ISO的Estelle或是CCITTO的SDL。因此，依據我們所提出的漸進式最大擴展協定驗證方法，我們在SUN SPARC工作站上已發展出一套名為Estelle-basedIncremental Maximal Progress Protocol Verification System，簡稱EIMPVS。依此方式，協定設計者可以使用我們所發展的EIMPVS去驗證他們所設計的通信協定有無邏輯錯誤存在。
• 英文摘要： Protocol verification is an activity involving detection of logical errors in communication protocols.In this paper, we propose an integrated approach, to protocol verification. We modify the CommunicatingFinite State Machine (CFSM)-based maximal progress state reduction technique so that it is ExtendedCommunicating Finite State Machine (ECFSM)-based. Next, we propose an ECFSM-based incrementalprotocol verification technique based on the maximal progress principle. To further reduce the numberof global states to be explored, the dead and live variables concept is incorporated. As a result, anincremental maximal progress protocol verification method is derived based on the integration approach.Our ECFSM-based method is, therefore, applicable to the ECFSM-based Formal Description Techniques(FDTs), e.g.，the International Standard Organization's (ISO) Estelle or International Telegraph andTelephone Consultative Committee's (CCITT) Specification and Description Language (SDL)．Based onthe incremental maximal progress verification method, an Estelle-based Incremental Maximal progressProtocol Verification System (EIMPVS) is developed-on SUN SPARC workstations. In this way, protocoldesigners can use our EIMPVS to verify Estelle-specified protocols．
• 中文關鍵字： computer networks; formal methods; protocol engineering; protocol verification; incremental verification; Estelle
• 英文關鍵字： --