Automatic Transformation of Cloud Computing Service Composition to Verifiable Models

Several information technology enterprises have decided to migrate into cloud for their computing and storage requirements in order to get reliable software and high performance hardware resources in a cost-effective manner. A single cloud service cannot ful fill the functional requirements in several real-world situations. Then, the concept of composite cloud service is introduced to bundle single cloud services to satisfy the complex end-users´ requirements. However, there is no formal approaches that can verify the behavioral correctness of cloud composite services automatically. In this paper, we address this shortcoming by developing an automatic transformation tool. This tool takes as input the BPEL processes in charge of the services composition and the behavior description of participating services and produces the ISPL+ models that include all possible interactions among participating agents through intermediate object representations. The tool also capitalizes on the most widely used BPEL constructs and includes a transformation algorithm for each BPEL construct. Our tool is the first one that considers the interactions among invoked services. Such interactions are formally modeled by the social commitment modality in the CTLC logic. The generated ISPL+ agent models can be verified using the MCMAS+ symbolic model checker developed for multi-agent communication.