Soutenance de Doctorat de Mr Oussama Kamel

Date : 3 June 2021
Place : Université Constantine 2
event.organized-by-team MFGL
Key words
Cloud Systems SLA BRS Modélisation Vérification NuSMV

tors and cloud services. Moreover, complex interactions and different types of compositions are defined among these entities. Service Level Agreements (SLAs) are used as the means to
regulate the relationships between the different actors and specify the expected level of services,
in terms of their functional and non-functional properties. Regarding this complexity and due
to the dynamic nature of cloud environments, ensuring the correctness of cloud systems is a
challenging task. In consequence, there is a need for techniques allowing formal description of
these entities and paving the way towards formal verification of their behaviors. This thesis lies
in the intersection between cloud computing and formal methods. Precisely, we show how to
apply formal methods in cloud computing encompassing the modeling and verification of systems
during SLA lifecycle.
In the first phase of the proposed approach, we address the modeling of the static structure
and the dynamic behavior of cloud systems using Bigraphical Reactive Systems (BRS). We show
that bigraphs are a powerful formalism that enables a faithful description of the different cloud
entities (including cloud actors, cloud services, and SLAs), the diversity of their properties, and
the complex interactions and dependencies among them. In addition, we propose a four-stage
SLA lifecycle, and define a set of bigraphical reaction rules to abstract these stages describing
the dynamic change of cloud entities’ states during the proposed lifecycle.
The second phase of this approach relies on the NuSMV model checker to verify that the
behavior of services and cloud actors cope with the SLA terms agreed during lifecycle of the SLA.
We consider two types of properties to be verified that are: liveness and safety. They express
desirable or undesirable behaviors of the different cloud entities during the SLA lifecycle. The
verification process is conducted in three steps. 1) We define a translation from bigraphical models
into SMV descriptions, the input language of NuSMV model checker. 2) Then, we express the
requirements expected as a set of liveness and safety properties using Linear Temporal Logic
(LTL) and Computation Tree Logic (CTL) formulas, and 3) we use the NuSMV model checker to
verify them. Finally, we define a case study on which we illustrate the application of our proposed