Synthesizing a protocol converter from executable protocol traces

Communicating finite state machines (CFSM´s) with FIFO (first in, first out) queues are used to model a protocol converter. A protocol conversion algorithm is developed and presented for the CSFM model of the protocols A and B. A converter H for protocols A=(A₀, A₁) and B=(B₀, B₁) is viewed as a black box such that H is between sender A ₀ and receiver B₁. This gives a resulting protocol X=(A₀, H, B₁). The conversion algorithm requires a specification of the message relationships between the messages of protocols A and B. It is assumed that protocols A and B have the required progress properties. The algorithm includes a search for related messages from the two protocols in an FIFO from a composite space formed by a Cartesian cross-product of state spaces A₁ and B₀. The search produces finite-length traces which are combined to form a state machine H, which is examined for freedom from unspecified receptions, deadlocks, and livelocks. A protocol conversion example demonstrates the applicability of the algorithm