TY - GEN
T1 - ECFSM-based maximal progress protocol verification
AU - Huang, Chung Ming
AU - Hsu, Jenq Muh
PY - 1993/12/1
Y1 - 1993/12/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0027814909&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0027814909&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:0027814909
SN - 0780312333
T3 - Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering
SP - 527
EP - 530
BT - Proceedings of the 10th IEEE Region Conference on Computer, Communication, Control and Power Engineering
PB - Publ by IEEE
T2 - Proceedings of the 1993 IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering (TENCON '93). Part 1 (of 5)
Y2 - 19 October 1993 through 21 October 1993
ER -