Sla-Driven Modeling And Verifying Cloud Systems: A Bigraphical Reactive Systems-Based Approach

We propose a formal approach based on Bigraphical Reactive Systems (BRSs) and model checking techniques for modeling and verifying the interaction behaviours of SLA-based cloud computing systems. In the first phase of this approach, we address the modeling of the static structure and the dynamic behavior of cloud systems using BRSs. We show how bigraphs enable the description of the different cloud entities, including cloud actors, cloud services, Service Level Agreements (SLAs), the diversity of their properties, and the complex interactions and dependencies among them. Furthermore, we propose a four-stages SLA lifecycle, and define a set of bigraphical reaction rules to abstract these stages and model the dynamic nature of the cloud. The second phase of this approach verifies that the behavior of services and cloud actors will cope with the agreed SLA terms during the lifecycle of the SLA. We map the proposed bigraphical models into SMV descriptions. Then, we express the interaction behaviors as a set of liveness and safety properties using Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) formulas, and we use the NuSMV model checker to verify them. Finally, we define a case study on which we illustrate the application of our proposed approach.