This paper proposes a method for deriving protocol specifications in a communicating processes model, in which protocol specifications are modeled by finite automata communicating through the LOTOS multirendezvous mechanism. Message sequence charts (MSCs) are used for the derivation inputs. MSCs are graphical representations of traces of protocols and are suitable for defining requirements. Since an MSC usually covers only partial behavior, several mechanisms for composing a large number of MSCs from element MSCs have been proposed. These mechanisms, however, are not adequate: Either their input language for MSCs is not powerful enough, or they need some information on protocol specifications (i.e., implementation specifications). This paper proposes the use of regular expressions over MSCs to fully define protocols. The proposed language is powerful enough to describe protocols in the communicating processes model. A derivation algorithm based on a finite automata construction algorithm that accept sets expressed by regular expressions is presented. Because the derived protocols sometimes include unrequired behavior, an algorithm for detecting unrequired behavior is also presented.

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.