Formal techniques for synthesizing a converter by inserting synchronization points into two given protocols are presented. Each synchronization point consists of a pair of asynchronous communication operations PUT and GET. The PUT operation inserts a message into a non-FIFO buffer, and then the GET operation retrieves and converts the message in the buffer. The PUT and GET operations may create some problems for the buffer: (1) channel overflow, that is the number of messages stored in the buffer exceeds its capacity; (2) improper termination, that is, the protocol terminates with some message left over in the buffer. Therefore, the resultant converter must be validated so that it is free from such protocol errors as channel overflow and improper termination. Several techniques for optimizing the computing time and space spent in validating a converter are proposed. >
