Distributed execution of a service often means that various places compete for the right to progress. If they exchange the right by explicit communication, there is a continuous flow of protocol messages. If the maximum transit delay of the communication medium is short, a better solution is to restrict progress of places to their individual time windows. The paper describes how to derive such time-sharing-based multi-party protocols for well-formed services specified in LOTOS/T+. The method is compositional with respect to the structure of the given service specification, supporting alternative, sequential, interrupt and parallel composition of services.

A stepwise refinement method of communications service specifications is proposed to generate communications software that can conform to any network architecture. This method uses a two-layered language; one layer is a service specification description language (STR), and the other layer is a supplementary specification description language for implementing STR description on a communications system (STR/D). STR specifies terminal behaviors that can be recognized from a perspective outside of the communications systems. With STR, a communications service is defined by a set of rules that can be described without detailed knowledge of communications systems or communications network architectures. Each STR rule describes a global state transition of terminals. Supplementary specifications, such as terminal control and network control, are needed to implement communications services specified by STR rules. These supplementary specifications are described by STR/D rules. Communications services, such as UPT (Universal Personal Telecommunication), are standardized so that they can be provided on a given functional model consisting of functional entities. Specifications for each functional entity in a network are obtained from the two kinds of initially described specifications mentioned above. The obtained specifications are described by STR(L) and STR/D(L) rules, which specify local specifications of a functional entity. These specifications for functional entities are then transformed into software specifications, and finally communications software is generated from these software specifications. This stepwise refinement method makes it possible to generate communications software that can conform to any functional model from service specifications.

In the conventional protocol synthesis, it is generally assumed that primitives in service specifications cannot be executed simultaneously at different Service Access Points (SAPs). Thus if some primitives are executed concurrently, then protocol errors of unspecified receptions occur. In this paper, we try to extend a class of service specifications from which protocol specifications are synthesized by the previous methods. We first introduce priorities into primitives in protocol specification so that it always selects exactly one primitive of the highest priority from a set of primitives that can be executed simultaneously, and executes it. Then, based on this execution ordering, we propose a new protocol synthesis method which can avoid protocol errors due to message collisions, communication competitions and so on. By applying the proposed synthesis method, we can automatically synthesize a protocol specifications from a given service specification which includes an arbitraty number of processes and allows parallel execution of primitives.

In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of connunication protocols.

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.

Responsive protocols are communication protocols which ensure timely and reliable recovery when error events occur. Protocol synthesis for design of responsive protocols is to derive a protocol specification based on a service specification. In the previous methods, if the service specification includes simultaneous transmission of primitives from a high layer to a low layer through different service access points, then the derived protocol specification includes protocol errors of unspecified reception caused by message collisions. Also, they only includes a recovery function such as retransmission of messages. This is not enough for recovery from abnormal states due to coordination loss. This paper extends a class of derived protocol specifications to include message collisions which usually occur in real communication protocols. Furthermore, this paper proposes a new method for synthesis of a responsive protocal specification derived from a service specification such that the derived protocol specification is free from protocol erros of unspecified receptions caused by message collisions and includes two recovery functions: message retransmission and checkpoint restart functions.