Incremental maximal progress protocol verification for ECFSM-based protocols

Chung-Ming Huang, Jenq Muh Hsu

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)600-615
Number of pages16
JournalProceedings of the National Science Council, Republic of China, Part A: Physical Science and Engineering
Volume22
Issue number5
Publication statusPublished - 1998 Sep

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'Incremental maximal progress protocol verification for ECFSM-based protocols'. Together they form a unique fingerprint.

  • Cite this