Incremental maximal progress protocol verification for ECFSM-based protocols

Chung-Ming Huang, Jenq Muh Hsu

研究成果: Article同行評審

摘要

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 SUN SPARC workstations. In this way, protocol designers can use our EIMPVS to verify Estelle-specified protocols.

原文English
頁(從 - 到)600-615
頁數16
期刊Proceedings of the National Science Council, Republic of China, Part A: Physical Science and Engineering
22
發行號5
出版狀態Published - 1998 九月

All Science Journal Classification (ASJC) codes

  • 工程 (全部)

指紋

深入研究「Incremental maximal progress protocol verification for ECFSM-based protocols」主題。共同形成了獨特的指紋。

引用此