Synthesis of Communicating Finite-State Machines with Guaranteed Progress

Abstract

We present a methodology to synthesize two communicating finite-state machines which exchange messages over two one-directional, FIFO channels. The methodology consists of two algorithms. The first algorithm takes one machineM, and constructs two communicating machinesM'andN'such that 1)M'is constructed fromMby adding some receiving transitions to it, and 2) the communication betweenM'andN'is bounded and free from deadlocks, unspecified receptions, nonexecutable transitions, and state ambiguities. The second algorithm takes the two machinesM'andN'which result from the first algorithm, and computes the smallest possible capacities for the two channels between them. Both algorithms require anO(st)time, wheresis the number of states in the given machineM, andtis the number of state transitions inM; thus, the methodology is practical to use.

Keywords

This publication has 13 references indexed in Scilit:

Protocol Validation by Maximal Progress State Exploration
IEEE Transactions on Communications, 1984
Unboundedness detection for a class of communicating finite-state machines
Information Processing Letters, 1983
On Communicating Finite-State Machines
Journal of the ACM, 1983
Deadlock Detection for a Class of Communicating Finite State Machines
IEEE Transactions on Communications, 1982
A Validation Technique for Tightly Coupled Protocols
IEEE Transactions on Computers, 1982
An improved protocol validation technique
Computer Networks (1976), 1982
Towards Analyzing and Synthesizing Protocols
IEEE Transactions on Communications, 1980
Formal Methods in Communication Protocol Design
IEEE Transactions on Communications, 1980
Protocol Validation by Duologue-Matrix Analysis
IEEE Transactions on Communications, 1978
An Automated Technique of Communications Protocol Validation
IEEE Transactions on Communications, 1978