A protocol converter can be regarded as a mapping between messages of two protocols. This mapping can be characterized by a set K of coupled significant messages. In the present paper a formal definition of the protocol converter with respect to K is given, and proposes a method for constructing the converter which is based on the coupled product of two finite state machines. The correctness of the method is proved.