Towards A Formal Modeling Of Cloud Services During The Life-Cycle Of Service Level Agreement

Service Level Agreement (SLA) represents a means of regulating and controlling the interaction between service providers and their customers. In the first part of this paper, we use Bigraphical Reactive Systems (BRS) to model customers, offered services by different providers and the SLA between them. Concretely, we use bigraphs, the static structure of BRS, to model these entities and to describe their relationships. In addition, we propose a set of reaction rules to show the evolution of their states during the different stages of the SLA's lifecycle. In the second part, we apply these models in the domain of cloud computing. Cloud computing architecture is usually represented as a stack of different layers. We show that the proposed models can be applied to any computing model (e.g., Software as a Service, Platform as a Service and Infrastructure as service layer) and they allow describing the SLA across the cloud stack layers. We show also that these models can represent the composition of services from several layers to offer complete solutions to end users.