To correct communicating finite state machines

A number of methods have been proposed to validate the communication between processes which exchange messages through bounded FIFO channels. However design criteria and rules are developed to construct correct protocols. In this paper, our objective is to propose a new correcting method for a pair of communicating finite state machines and we ensure that the communication is perfect and progresses indefinitely i.e deadlock-free, liveness, bounded, and without noexecutable transitions, unspecified receptions. The time complexity is bounded by O(nm) where n is the number of states and m is the number of transitions of a given machine. The first method is defined by adding receiving transitions and in the second we complete our results by adding sending transitions , then we obtain symmetric and isomorphic machines with unbounded communication.