ECFSM-based maximal progress protocol verification

Chung Ming Huang, Jenq Muh Hsu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

A number of protocol verification reduction techniques were proposed in the past. Most of these techniques are suitable for verifying communicating protocols specified in the Communicating Finite State Machine (CFSM) model. However, it is impossible to formally specify communicating protocols with predicates and variables using the CFSM model. The Extended Communicating Finite State Machine (ECFSM) model, which incorporates the mechanism for representing variables and predicates, can formally model communicating protocols with variables and predicates. To have more efficient verification for ECFSM-specified protocols, we propose an integrated ECFSM-based global state reduction technique in this paper. This new method is based on two techniques: the dead variables analysis which can reduce the number of global states, and the ECFSM-based maximal progress state exploration which can speed up the global state reachability analysis. Using our new ECFSM-based method, the maximal progress protocol verification can be directly applied to the Formal Description Techniques (FDTs) which are based on the extended state transition model, i.e., ISO's Estelle and CCITT's SDL.

Original languageEnglish
Title of host publicationProceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering
PublisherPubl by IEEE
Pages527-530
Number of pages4
ISBN (Print)0780312333
Publication statusPublished - 1993 Dec 1
EventProceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5) - Beijing, China
Duration: 1993 Oct 191993 Oct 21

Publication series

NameProceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering

Other

OtherProceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5)
CityBeijing, China
Period93-10-1993-10-21

All Science Journal Classification (ASJC) codes

  • Engineering(all)

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

Cite this