![Sample our Bioscience journals, sign in here to start your access, Latest two full volumes FREE to you for 14 days]({"type":"image" , "src" : "/sda/5925/TOC-Subject-Sample-2021-Bioscience.jpg"})
Abstract
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.
2010 AMS Subject Classification: