Automatic Transformation of Cloud Computing Service Composition to Verifiable Models

Ana Vazquez, Mohamed El Menshawy, Jamal Bentahar

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageBritish English
Title of host publicationProceedings - 2015 International Conference on Future Internet of Things and Cloud, FiCloud 2015 and 2015 International Conference on Open and Big Data, OBD 2015
EditorsMuhammad Younas, Irfan Awan, Massimo Mecella
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages173-180
Number of pages8
ISBN (Electronic)9781467381031
DOIs
StatePublished - 19 Oct 2015
Event3rd International Conference on Future Internet of Things and Cloud, FiCloud 2015 - Rome, Italy
Duration: 24 Aug 201526 Aug 2015

Publication series

NameProceedings - 2015 International Conference on Future Internet of Things and Cloud, FiCloud 2015 and 2015 International Conference on Open and Big Data, OBD 2015

Conference

Conference3rd International Conference on Future Internet of Things and Cloud, FiCloud 2015
Country/TerritoryItaly
CityRome
Period24/08/1526/08/15

Keywords

  • Cloud computing service
  • formal verification
  • ISPL+ agent models
  • transformation algorithms

Fingerprint

Dive into the research topics of 'Automatic Transformation of Cloud Computing Service Composition to Verifiable Models'. Together they form a unique fingerprint.

Cite this