INTERACTIVE PROTOCOL SYNTHESIS ALGORITHM USING A GLOBAL STATE TRANSITION GRAPH.

Yao Xue Zhang; Kaoru Takahashi; Norio Shiratori; Shoichi Noguchi

doi:10.1109/32.4659

INTERACTIVE PROTOCOL SYNTHESIS ALGORITHM USING A GLOBAL STATE TRANSITION GRAPH.

Yao Xue Zhang^*, Kaoru Takahashi, Norio Shiratori, Shoichi Noguchi

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

20 Citations (Scopus)

Abstract

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.

Original language	English
Pages (from-to)	394-404
Number of pages	11
Journal	IEEE Transactions on Software Engineering
Volume	14
Issue number	3
DOIs	https://doi.org/10.1109/32.4659
Publication status	Published - 1988 Mar

ASJC Scopus subject areas

Computer Graphics and Computer-Aided Design
Software
Electrical and Electronic Engineering

Access to Document

10.1109/32.4659

Cite this

@article{3fa0f486cfa04061ac3a96d1d7a700ef,

title = "INTERACTIVE PROTOCOL SYNTHESIS ALGORITHM USING A GLOBAL STATE TRANSITION GRAPH.",

abstract = "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.",

author = "Zhang, {Yao Xue} and Kaoru Takahashi and Norio Shiratori and Shoichi Noguchi",

year = "1988",

month = mar,

doi = "10.1109/32.4659",

language = "English",

volume = "14",

pages = "394--404",

journal = "IEEE Transactions on Software Engineering",

issn = "0098-5589",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

number = "3",

}

TY - JOUR

T1 - INTERACTIVE PROTOCOL SYNTHESIS ALGORITHM USING A GLOBAL STATE TRANSITION GRAPH.

AU - Zhang, Yao Xue

AU - Takahashi, Kaoru

AU - Shiratori, Norio

AU - Noguchi, Shoichi

PY - 1988/3

Y1 - 1988/3

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0023978660&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0023978660&partnerID=8YFLogxK

U2 - 10.1109/32.4659

DO - 10.1109/32.4659

M3 - Article

AN - SCOPUS:0023978660

SN - 0098-5589

VL - 14

SP - 394

EP - 404

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

IS - 3

ER -

INTERACTIVE PROTOCOL SYNTHESIS ALGORITHM USING A GLOBAL STATE TRANSITION GRAPH.

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this