In this paper the analyse of reachability tree for protocol errors exploration is presented. The state perturbation technique is based on the reachability analysis. The communicating processes are modeled as finite state machines. The base for the automatic protocol verification are formal methods. The protocols specification can be rigorously analyzed for completeness and consistency. By the protocol verificator "PERTURB" the given system state is systematically perturbed to find out all possible states, so that the new states become states for further perturbation. The states produced in that way are systematically examined if they contain errors, until all reachable states are passed. The perturbation technique applied in this paper successfully detects deadlock states, ambiguities, unspecified receptions, non executable interactions and channel overflows. Finally, on test protocol all kinds of errors are generated and then successfully detected. |