ECFSM-based maximal progress protocol verification

Chung Ming Huang, Jenq Muh Hsu

研究成果: Conference contribution

摘要

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.

原文English
主出版物標題Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering
發行者Publ by IEEE
頁面527-530
頁數4
ISBN(列印)0780312333
出版狀態Published - 1993 十二月 1
事件Proceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5) - Beijing, China
持續時間: 1993 十月 191993 十月 21

出版系列

名字Proceedings 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)
城市Beijing, China
期間93-10-1993-10-21

All Science Journal Classification (ASJC) codes

  • Engineering(all)

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

引用此