An interactive synthesis algorithm, to construct two communicating finite-state machines (protocols), is presented. The machines exchange messages over two unidirectional FIFI (first-in first-out) channels when the function of the protocol has been given. The synthesis algorithm first constructs the global state transition graph (GSTG) of a protocol 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 processes. 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.
ASJC Scopus subject areas
- コンピュータ グラフィックスおよびコンピュータ支援設計