This paper proposes an algorithm for optimizing concurrent program specification generated by design automation techniques. Some of the information in automatically generated specifications can be modified for optimization. The proposed algorithm changes some signals between processes. The computational complexity of the algorithm is O(nlogn), where n is the number of states in a given process specification. Experimental application results demonstrate it useful not only to optimize individual process descriptions but also to change signals transferred between processes in the optimization.

An extended state transition model and verification algorithm are proposed for specification and verification of protocols. The state transition model is an extention of Zafiropulo's two process protocol model to specify protocols designed for communication between more than two processes. A concept of Reduced Implementation Sequence (RIS)" is introduced to establish a protocol verification algorithm. By using RIS, potential movements of modeled systems are compactly described and the computation time necessary for verification becomes much shorter than that required for the method based on the traditional reachability analysis.

This paper presents a language called SAL (Service Addition Language) which is used to describe protocol-oriented service specifications for communications software. This language has the following features: (1) Formal representation of the message sequence diagram: An individual service can be specified in an algebraic form of message sequence diagrams which are widely used in service design. (2) Separate description of services: New services to be added can be specified without the necessity of referring to the existing services. The synthesizer utility for SAL is prepared to detect any inconsistent relationship between the new and existing services. (3) Transformability into CCITT SDL (Specification and Description Language) document: As new service specifications are integrated with existing ones, functional specifications in SDL are automatically extended to implement the new along with the existing services. This is also done by the synthesizer. The algorithm is presented, which detects inconsistent relations between services, and a considerable amount of effort for service addition is shown to be automatable by introducing SAL. SAL and its supporting utilities are intended to be integrated into a development and maintenance environment called a Systems Design Environment (SDE) for communications software. SDE has a utility which generates program codes for the processes defined by the SDL documents which are derived from SAL description.

A service specification description method for communication control machines (CCM), called the multilogue-set method", is proposed. This method is well suited for the discussion of the CCM renewal in response to service addition requests.

A process algebra dACP based on differential equivalence (d-equivalence) and the algebra ACP by Bergstra et al. is proposed. The features of dACP are as follows:Real parallelism can be distiguished from action interleaving.Action refinement is possible under d-equivalence. Thus, dACP resolves the difficulties of ACP caused by the atomicity of actions assumed in ACP. After defining dACP, d-equivalence is shown to imply the original equivalence defined in ACP. Next, it is shown that action refinement can be introduced in a natural way under d-equivalence.

Multiple communication Bus Network (MCNET) is proposed. This network interconnect, all exchanges in a specified area by one large scale transmission line to aim at network cost reduction and to secure adaptability for traffic variation.