An interactive protocol synthesis algorithm using a global state transition graph

Author

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

Author_Institution

Res. Inst. of Electr. Commun., Tohoku Univ., Sendai, Japan

Volume

14

Issue

3

fYear

1988

fDate

3/1/1988 12:00:00 AM

Firstpage

394

Lastpage

404

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

Keywords

finite automata; graph theory; interactive programming; protocols; buffer overflow; complete reception; deadlock avoidance rules; deadlock freeness; finite-state machines; global state transition graph; interactive protocol synthesis algorithm; production rules; Algorithm design and analysis; Automata; Buffer overflow; Protocols; System recovery;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.4659

Filename

4659