Article
Journal :
Computer Standards & Interfaces
ISSN : 0920-5489
Publisher :
Information
Period : September 2020
Volume : 74
Details
SLA-Driven Modeling and Verifying Cloud Systems: A Bigraphical Reactive Systems-based Approach
Oussama Kamel Allaoua Chaoui Gregorio Diaz Mohamed Gharzouli
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.
Key words :
Cloud computing SLA Bigraph Bigraphical reactive systems NuSMV Formal verification
Ref. laboratory citation :
misc-lab-344
DOI :
https://doi.org/10.1016/j.csi.2020.103483
Link :
Texte intégral
ACM :
O. Kamel, A. Chaoui, G. Diaz and M. Gharzouli. 2020. SLA-Driven Modeling and Verifying Cloud Systems: A Bigraphical Reactive Systems-based Approach. Computer Standards & Interfaces, 74 (September 2020), Elsevier. DOI: https://doi.org/https://doi.org/10.1016/j.csi.2020.103483.
APA :
Kamel, O., Chaoui, A., Diaz, G. & Gharzouli, M. (2020, September). SLA-Driven Modeling and Verifying Cloud Systems: A Bigraphical Reactive Systems-based Approach. Computer Standards & Interfaces, 74, Elsevier. DOI: https://doi.org/https://doi.org/10.1016/j.csi.2020.103483
IEEE :
O. Kamel, A. Chaoui, G. Diaz and M. Gharzouli, "SLA-Driven Modeling and Verifying Cloud Systems: A Bigraphical Reactive Systems-based Approach". Computer Standards & Interfaces, vol. 74, Elsevier, September, 2020. DOI: https://doi.org/https://doi.org/10.1016/j.csi.2020.103483.
BibTeX :
@article{misc-lab-344,
author = {Kamel, Oussama and Chaoui, Allaoua and Diaz, Gregorio and Gharzouli, Mohamed},
title = {SLA-Driven Modeling and Verifying Cloud Systems: A Bigraphical Reactive Systems-based Approach},
journal = {Computer Standards & Interfaces},
volume = {74},
issn = {0920-5489},
publisher = {Elsevier},
year = {2020},
month = {September},
doi = {https://doi.org/10.1016/j.csi.2020.103483},
url = {https://www.sciencedirect.com/science/article/abs/pii/S092054892030369X},
keywords = {Cloud computing, SLA, Bigraph, Bigraphical reactive systems, NuSMV, Formal verification}
}
RIS :
TI  - SLA-Driven Modeling and Verifying Cloud Systems: A Bigraphical Reactive Systems-based Approach
AU - O. Kamel
AU - A. Chaoui
AU - G. Diaz
AU - M. Gharzouli
PY - 2020
SN - 0920-5489
JO - Computer Standards & Interfaces
VL - 74
PB - Elsevier
AB - 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.
KW - Cloud computing
KW - SLA
KW - Bigraph
KW - Bigraphical reactive systems
KW - NuSMV
KW - Formal verification
DO - https://doi.org/10.1016/j.csi.2020.103483
UR - https://www.sciencedirect.com/science/article/abs/pii/S092054892030369X
ID - misc-lab-344
ER -