Issue No. 03 - March (1988 vol. 14)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.4659
<p>An interactive synthesis algorithm, to construct two communicating finite-state machines (protocols), is presented. The machines exchange messages over two unidirectional FIFO (first-in first-out) channels when the function of the protocol has been given. The synthesis algorithm first constructs the global state transitiion graph (GSTG) of a protoco to be synthesized and then produces the protocol. It is based on a set of production rules and a set of deadlock avoidance rules, which guarantee that complete reception and deadlock freeness capabilities are provided in the interacting process. This synthesis algorithm prevents a designer from creating unspecified reception and nonexecutable transition, avoids the occurrence of deadlocks, and monitors for the presence of buffer overflow.</p>
interactive protocol synthesis algorithm; global state transition graph; finite-state machines; global state transition graph; production rules; deadlock avoidance rules; complete reception; deadlock freeness; buffer overflow; finite automata; graph theory; interactive programming; protocols
K. Takahashi, S. Noguchi, N. Shiratori and Y. Zhang, "An Interactive Protocol Synthesis Algorithm Using a Global State Transition Graph," in IEEE Transactions on Software Engineering, vol. 14, no. , pp. 394-404, 1988.