Khaled Khebbeb

Research interests

• Formal Modeling
• Elasticity
• Strategies
• Bigraphical Reactive Systems
• Cloud Computing

Projects

Thesis

Title

Formal Modeling and Verification of Elastic Behaviors in Cloud Systems

Description

Elasticity property allows Cloud systems to adapt to their incoming workload by provisioning and de-provisioning computing resources in an autonomic manner, as the demand rises and drops. However, due to the unpredictable nature of the workload and the numerous factors that impact elasticity, providing accurate action plans to insure a Cloud system’s elasticity while preserving high level policies (performance, costs) is a particularly challenging task. 

This thesis aims to provide a thorough specification and implementation of Cloud systems, by relying on bigraphs as a formal model, over two aspects: structural (1) and behavioral (2). The encoding of these specifications and their implementation are defined in Rewrite Logic via Maude language.

Structurally, the goal is to define a correct modeling of Cloud systems’ "back-end" structure. This part is supported by the specification capabilities of Bigraph formalism. Specifically, via "sorting" mechanisms and construction rules that allow defining the designer’s desiderata.

As for the behavioral part, it consists of model, implement and validate generic auto-scaling strategies in order to describe the elastic auto-adaptive mechanisms of Cloud systems (horizontal and vertical scaling, migration, etc.) at different levels (service and infrastructure). These tasks are supported by the dynamic aspects of Bigraphical Reactive Systems (BRS) formalism (through reaction rules). 

Members

Publications

Publications via DBLP