Issue No. 04 - April (1991 vol. 40)

ISSN: 0018-9340

pp: 487-499

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.88468

ABSTRACT

<p>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/sub 0/, A/sub 1/) and B=(B/sub 0/, B/sub 1/) is viewed as a black box such that H is between sender A/sub 0/ and receiver B/sub 1/. This gives a resulting protocol X=(A/sub 0/, H, B/sub 1/). 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/sub 1/ and B/sub 0/. 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.</p>

INDEX TERMS

protocol convertor synthesis; executable protocol traces; finite state machines; queues; model; protocol conversion algorithm; conversion algorithm; message relationships; Cartesian cross-product; state spaces; deadlocks; livelocks; finite automata; protocols.

CITATION

M. Rajagopal, R.E. Miller, "Synthesizing a Protocol Converter From Executable Protocol Traces",

*IEEE Transactions on Computers*, vol. 40, no. , pp. 487-499, April 1991, doi:10.1109/12.88468