Research
I am mainly interested in rigorous specification and verification of self-adaptive and self-managed (autonomic) software systems. I focus essentially on the formalization, the de-complexification, the verification and the quantitative analysis of the main self-* properties (such as self-awareness, self-stabilization, etc.) in Cloud, service-oriented systems and more recently, in Fog/Edge systems.Formalization and evaluation of cross-layer elasticity strategies in the Cloud
(my Ph.D. project - defended on June 29th 2019)
During my Ph.D., I worked within the
MOVIES team @
LIUPPA lab
and the
GLSD team @
LIRE lab,
on the formalization of the
Elasticity property
within
Cloud-based systems. Precisely, I investigated the expressiveness and specification capabilities
of the Bigraphical Reactive Systems
formalism (BRS for short) into the formalization of the elastic behaviors
of Cloud systems, as an use-case of autonomic complex software systems.
Results of my research project have shown that the BRS are particularly powerful in terms of structural and behavioral modeling and decomplexification of such systems design. Ultimately, I have developed a complete formal-based methodology to design and analyze different composable high-level behaviors (i.e., strategies) to manage Cloud elasticity.
The proposed methodology involves an original and complementary combination of different formalisms/formal modeling languages and mathematical logics/theories, namely: Bigraphical Reactive Systems, Rewriting logic , Maude, Linear temporal Logic (LTL) and Queuing theory, to develop three main design phases: Formal modeling, Qualitative verification and Quantitative analysis, as follows.
In addition, the system evolution over time (i.e., reconfiguration) was modeled using a set of Bigraphical Reaction Rules, which express the system's adaptation capabilities (horizontal, vertical scaling, migration and load-balancing at different Cloud levels) as structural (graph-based) restructuration (rewriting).
Given the rewriting-based semantics of the BRS formalism, I proposed a way to enrich the BRS specifications in terms of quantitative considerations (e.g.: hosting thresholds, load, etc.) using the Maude formal specification language, which is an implementation of the Rewriting logic.
Maude enables designing conditional rewriting rules (which encode and extend the Bigraphical reaction rules expressiveness) to define different elasticity strategies (i.e., high level behaviors) which are of an autonomic triggering nature.
Such behavioral modeling enables the formalization of the Self-* properties such as self-management and self-adaptation. The rewriting rules' triggering conditions were expressed in First-order logic, which enables formalizing the self-awareness property.
As Maude enables the executability of the defined behaviors, the verification process was performed using the Maude-integrated LTL model-checker (see documentation). Maude allows associating a Kripke structure to the defined specifications in order to identify the desirable and undesirable system states.
Globally, the conducted verification goes towards ensuring the fundamental Liveness property associated to the defined behaviors, as a qualitative indicator of their correctness.
The performed experimental study showed that the defined elasticity strategies can be composed in a complementary way to obtain complex behaviors (i.e., different patterns in terms of cost, performance and efficency).
The obtained results were validated using the Erlang C formula. Their analysis showed that different strategies combinations result in different high-level policies such as High performance, High economy, High infrastructure availability, Infrastructure costs optimization and High resource efficiency.
Results of my research project have shown that the BRS are particularly powerful in terms of structural and behavioral modeling and decomplexification of such systems design. Ultimately, I have developed a complete formal-based methodology to design and analyze different composable high-level behaviors (i.e., strategies) to manage Cloud elasticity.
The proposed methodology involves an original and complementary combination of different formalisms/formal modeling languages and mathematical logics/theories, namely: Bigraphical Reactive Systems, Rewriting logic , Maude, Linear temporal Logic (LTL) and Queuing theory, to develop three main design phases: Formal modeling, Qualitative verification and Quantitative analysis, as follows.
Formal modeling
BRS were used to rigorously build Cloud system stuctures through a sorting discipline and construction rules, which represent a designer's desiderata (axioms).In addition, the system evolution over time (i.e., reconfiguration) was modeled using a set of Bigraphical Reaction Rules, which express the system's adaptation capabilities (horizontal, vertical scaling, migration and load-balancing at different Cloud levels) as structural (graph-based) restructuration (rewriting).
Given the rewriting-based semantics of the BRS formalism, I proposed a way to enrich the BRS specifications in terms of quantitative considerations (e.g.: hosting thresholds, load, etc.) using the Maude formal specification language, which is an implementation of the Rewriting logic.
Maude enables designing conditional rewriting rules (which encode and extend the Bigraphical reaction rules expressiveness) to define different elasticity strategies (i.e., high level behaviors) which are of an autonomic triggering nature.
Such behavioral modeling enables the formalization of the Self-* properties such as self-management and self-adaptation. The rewriting rules' triggering conditions were expressed in First-order logic, which enables formalizing the self-awareness property.
Qualitative verification
The introduced behaviors were verified formally through a state-based model-checking technique supported by the Linear temporal logic (LTL).As Maude enables the executability of the defined behaviors, the verification process was performed using the Maude-integrated LTL model-checker (see documentation). Maude allows associating a Kripke structure to the defined specifications in order to identify the desirable and undesirable system states.
Globally, the conducted verification goes towards ensuring the fundamental Liveness property associated to the defined behaviors, as a qualitative indicator of their correctness.
Quantitative analysis
To analyze the hypothetical outcomes of the designed behaviors (elasticity strategies) in terms of cost, performance and efficiency, I proposed a simulation-based experimental methodology using the Queuing theory.The performed experimental study showed that the defined elasticity strategies can be composed in a complementary way to obtain complex behaviors (i.e., different patterns in terms of cost, performance and efficency).
The obtained results were validated using the Erlang C formula. Their analysis showed that different strategies combinations result in different high-level policies such as High performance, High economy, High infrastructure availability, Infrastructure costs optimization and High resource efficiency.
- Software: The simulation-based methodology and the defined elasticity behaviors
were consolidated within a home-made tool. I am currently working
on a GUI for the tool,
it will soon be available under the
software section.
- Scientific production: My Ph.D. thesis and publications are available under the publications section.
Recently
I am working on extending and refining the methodology I developed during my Ph.D. to consider
resource management in the IoT/Edge/Fog/Cloud landscape.
I have recently submitted a journal article which studies the orchestration of Cloud and Fog self-adaptation behaviors in terms of resource management
(more details under the publications section).
I have recently submitted a journal article which studies the orchestration of Cloud and Fog self-adaptation behaviors in terms of resource management
(more details under the publications section).
Back to Top !