A design and verification framework for service composition in the cloud

The service cloud model allows hosted services to be dynamically provisioned and composed as part of larger, more complex cloud applications. Compatibility of interaction and quality of service are important to provisioning similar services available in the cloud to a client request. Auditing individual services, the composition and its outcome, and the overall cloud resources, used for monetary assessment or to ensure critical operations, also provide properties for reasoning over service and composition capabilities. Security policies and potential violations pose a threat to the composition since sensitive data may be leaked if information flow control guarantees cannot be proven. Service engineering lacks design principles and an expression infrastructure for formal representation and reasoning within a service cloud model. Reasoning over service compositions requires a formal language that can express multiple service and cloud properties. In this paper, we use coordination language techniques to express services, their interaction capabilities and information sharing constraints, and the infrastructure of a service cloud model in which services can be accurately provisioned, composed and reasoned over to provide necessary guarantees. We discuss lessons learned from the process of formulating the service representation and cloud model infrastructure.