Incremental protocol verification method

Chung-Ming Huang, Jenq Muh Hsu

Research output: Contribution to journalArticle

12 Citations (Scopus)

Abstract

Protocol verification is an activity to assure the correctness of communication protocols. Global state reachability analysis is one of the most straightforward and easily automated protocol verification methods. This paper proposes an incremental protocol verification method for the Extended Communicating Finite State Machine (ECFSM) model. Incremental protocol verification allows protocols to be modified at the run time of global state reachability analysis. Then, instead of re-exploring the modified protocols from scratch, global state reachability analysis is continued incrementally at the modification point. To enhance the efficiency, the proposed method incorporates the dead and live variables concept that is used in Chu and Liu's global state reduction technique. Using the proposed incremental protocol verification method, incremental protocol design environments are achievable for ECFSM-based Formal Description Techniques (FDTs), e.g. ISO's Estelle. Our application of the proposed method to Estelle is also briefly introduced in this paper.

Original languageEnglish
Pages (from-to)698-710
Number of pages13
JournalComputer Journal
Volume37
Issue number8
DOIs
Publication statusPublished - 1994 Jan 1

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Incremental protocol verification method'. Together they form a unique fingerprint.

  • Cite this