Controllability Preservation and Behavioural Refinement for Service Protocols

In this paper, we provide a new compositional framework for specifying controllability and refinement of service protocols interacting asynchronously. First, we investigate necessary and sufficient conditions for protocols controllability. Then, we give sufficient conditions for preserving controllability of protocols by asynchronous composition. Finally, we propose two protocols refinement relations and show the soundness of our formal framework: independent implement ability of protocols together with the preservation of controllability under protocols by refinement.