抄録
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.
| 本文言語 | English |
|---|---|
| ページ（範囲） | 394-404 |
| ページ数 | 11 |
| ジャーナル | IEEE Transactions on Software Engineering |
| 巻 | 14 |
| 号 | 3 |
| DOI | |
| 出版ステータス | Published - 1988 3月 |
ASJC Scopus subject areas
- コンピュータ グラフィックスおよびコンピュータ支援設計
- ソフトウェア
- 電子工学および電気工学