ON THE SPECIFICATION AND SYNTHESIS OF COMMUNICATING PROCESSES

An objective methodology for the specification and synthesis of communicating processes is presented. An earlier work describes how the analysis of these processes can be automated using a set of algebraic operators. Here we demonstrate that such operators can be used to express communicating processes in terms of behavioral constraints and that the corresponding state transition descriptions can be derived automatically, or synthesized, from these expressions. The behavioral constraints serve as high-level specifications for communicating processes. These constraints indicate the desired behavior of a process, possibly embedded in a system, by defining its range. The proposed approach is shown to be applicable to a common problem which concerns the synthesis of the central module serving a number of clients in a specific distributed system configuration.