An Incremental Protocol Verification Method | Zendy

C.-M. Huang | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

An Incremental Protocol Verification Method

Author(s) -

C.-M. Huang

Publication year - 1994

Publication title -

the computer journal

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.319

H-Index - 64

eISSN - 1460-2067

pISSN - 0010-4620

DOI - 10.1093/comjnl/37.8.698

Subject(s) - reachability , correctness , computer science , protocol (science) , model checking , state (computer science) , formal verification , finite state machine , formal methods , distributed computing , theoretical computer science , reduction (mathematics) , algorithm , programming language , mathematics , geometry , medicine , alternative medicine , pathology

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 reexploring the modified protocols from scratch, global state rechability 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 (Chu and Liu, 1989). 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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research