A compositional framework to the specification of service protocols controllability and substitutability

摘要

Service description aims at specifying syntactic and semantic properties of the service by distinguishing several interoperability levels (signature, interaction protocol, and semantics). However, providing a basic service description is not sufficient to facilitate the development of services and provide customized information. To do so, it is important to develop formal methods and sufficient software tools for analysing service description. This paper provides a new compositional framework for specifying controllability and substitutability of service protocols interacting asynchronously. First, we investigate necessary and sufficient conditions for protocols controllability and give sufficient conditions for preserving controllability by composition. Then, we propose two protocols substitutability relations and show the soundness of our formal framework. Finally, we propose two protocols refinement relations for checking our substitutability relations and show that the implementability of protocols under refinement is context-independent. We use INA and CADP tools to automatically verify the protocols controllability and substitutability via refinement.