An improved method for automatic validation of communication protocols

A novel relief strategy for reachability analysis which can reduce the state-space problem by combining states that have similar behavior into a single aggregate state representation is proposed. The proposed method can be considered as a new encoding scheme for reducing the state explosion problem. Three algorithms are proposed to perform the validation using the aggregate states representation. The method can be used to validate protocols specified in the communicating finite-state machine (CFSM) model and the extended finite-state machine (EFSM) model. It has the same analytical power as the conventional reachability analysis but requires less time and space than the conventional method