AUTOMATED SYNTHESIS OF PROTOCOL SPECIFICATIONS FROM SERVICE SPECIFICATIONS WITH PARALLELLY EXECUTABLE MULTIPLE PRIMITIVES

In the conventional protocol synthesis, it is generally assumed that p rimitives 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 specificati ons from which protocol specifications are synthesized by the previous methods. We first introduce priorities into primitives in protocol sp ecification so that it always selects exactly one primitive of the hig hest priority from a set of primitives that can be executed simultaneo usly, and executes it. Then, based on this execution ordering, we prop ose a new protocol synthesis method which can avoid protocol errors du e to message collisions, communication competitions and so on. By appl ying the proposed synthesis method, we can automatically synthesize a protocol specifications from a given service specification which inclu des an arbitrary number of processes and allows parallel execution of primitives.