頁籤選單縮合
題 名 | An Incremental Maximal Progress Protocol Verification for ECFSM-Based Protocols=以ECFSM為協定描述之漸進式最大擴展協定驗證 |
---|---|
作 者 | 黃崇明; 許政穆; | 書刊名 | Proceedings of the National Science Council : Part A, Physical Science and Engineering |
卷 期 | 22:5 1998.09[民87.09] |
頁 次 | 頁600-615 |
分類號 | 448.6 |
關鍵詞 | 協定描述; 最大擴展協定驗證; 通信協定; Computer networks; Formal methods; Protocol engineering; Protocol verification; Incremental verification; Estelle; |
語 文 | 英文(English) |
中文摘要 | 在通信協定領域中,協定驗證主要目的是在偵測通信協定在設計階段是否有邏輯 錯誤存在。在本論文中,我們提出一整合的協定驗證技術。首先我們提出一適用於ECFSM 為協定描述之最大擴展協定驗證(maximal progress protocol verification),並且將此協定驗證加 入漸進式的協定驗證方法。除此之外為了降低驗證過程中總體狀態的生成個數,我們亦整合 了dead and live變數分析技術來減少總體狀態的生成數目。所以,我們所提出的漸進式最大 擴展協定驗證,整合了數種的協定驗證技術所推導出來的。而在本論文中,我們所提出的以 ECFSM為協定驗證方法可以直接應用於以同樣以ECFSM為基礎的正規描述技術(Formal Description Techniques, FDTs),如ISO的Estelle或是CCITT的SDL。因此,依據我們所提 出的漸進式最大擴展協定驗證方法,我們在SUM SPARC工作站上已發展出一套名為 Estelle-based Incremental 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 Communicating Finite State Machine (CFSM)-based maximal progress state reduction technique so that it is Extended Communicating Finite State Machine (ECFSM)-based. Next, we propose an ECFSM-based incremental protocol verification technique based on the maximal progress principle. To further reduce the number of global states to be explored the dead and live variables concept is incorporated. As a result, an incremental 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 and Telephone Consultative Committee's (CCITT) Specification and Description Language (SDL). Based on the incremental maximal progress verification method, an Estelle-based Incremental Maximal progress Protocol Verification System (EIMPVS) is developed on SUM SPARC workstations. In this way, protocol designers can use our EIMPVS to verify Estelle-specified protocols. |
本系統中英文摘要資訊取自各篇刊載內容。