A Novel Technique for Synthesizing Distributed and Concurrent Protocol Specifications

摘要

Several methods have been proposed for synthesizing computer communication protocol specifications starting from service specifications. Some protocol synthesis methods based on the Finite State Machine (FSM) model assume that primitives in the service specifications cannot be executed simultaneously. Others either handle only controlled primitive concurrency or have tight restrictions on the applicable FSM topologies. This paper proposes a concurrent-based protocol synthesis method that eliminates the restrictions imposed by the earlier methods. The synthesis method uses a sequential-based synthesis method to derive a sequential protocol specification (P-SPEC) from a service specification (S-SPEC) and then applies several transformation rules to re-model the resulting P-SPEC to consider the concurrency behavior specified in the S-SPEC.