Synthesis of Protocol Specifications from Service Specifications of Distributed Systems in a Marked Graph Model
Hirozumi Yamaguchi, Kenichi Taniguchi, Kozo Okano, Teruo Higashino · OUKA (Osaka University Knowledge Archive) (Osaka University) · 1994
In a distributed system, the protocol entities must exchange some data values and synchronization messages in order to ensure the temporal ordering of the events described in a service specification for the distributed system. It is desirable that a correct protocol specification can be derived automatically from a given service specification. In this paper, we propose an algorithm which synthesizes automatically a correct protocol specification from a service specification described as a Marked Graph with Registers (MGR) model and resources (registers and gates) allocation information. This model has a finite control modeled as a marked graph. Therefore, parallel events can be described. In our method, to minimize the number of the exchanged messages, we use a procedure to calculate an optimum solution for 0-1 integer linear programming problems. The number of the steps which each protocol entity needs to simulate one transition in the service specification is also minimized. Ways to avoiding conflict of registers are also described. Our approach has the following advantages. First, parallel events can be described in a service specification. Secondly, many practical systems can be described in the MGR model. Finally, at the protocol specification level, we can understand what events can be executed in parallel.