Title :

First registration in January, 2017 at The Faculty of Economics Sciences and Management of Sfax.

Abstract :

Keywords:

Title : A refinement based approach for the integration of service composition models: From choreography to orchestration.

First registration in November, 2011 at The Faculty of Economics and Management of Sfax.

Title : Resources Provisioning for Dynamic Workflows in Cloud Computing.

Defended on March 24, 2018 at The Faculty of Economics Sciences and Management of Sfax.

Abstract : With the rapidly changing demands, Workflows have a vital need for dynamic adaptation in order to react quickly and easily to expected or unforeseen environmental perturbations. Cloud Computing has become an effective solution for deploying these Workflows with a high level of performance and low cost. Nevertheless, adopting the Cloud raises several challenges, particularly with regard to performance and correction. On the one hand, the optimal resources provisioning is not a trivial task given the dynamic changes of Workflows and the variety of often conflicting objectives. On the other hand, given the complexity of the studied applications, their modeling is more prone to errors on the part of the designers (deadlock, infinite executions, etc.). Thus, the main contributions of this thesis is articulated around two main parts. The first part consists in proposing two provisioning algorithms to manage Cloud resources for a dynamic Workflow while meeting the QoS requirements. The performance of these algorithms is evaluated in terms of different metrics. In the second part, we propose a formal model that verifies dynamic Workflows deployed in the Cloud. We specify and prove the correction of this model using the formal method Event-B.

Keywords: Workflow, dynamic changes, Cloud Computing, provisioning, resources, verification.

Title : A graph transformation based approach for the validation of checkpointing algorithms for distributed systems.

Defended on November 30, 2017 at The Faculty of Economics Sciences and Management of Sfax.

Abstract : With the evolution of technology, distributed systems have evolved and their verification has become more and more difficult. In this context, we suggest an approach for the Minimal and Compact Set Representation of Causal Dependencies based for Distributed Systems. Then, we present a tool as an implémentation of our approach. The MCSR tool was constructed as a library in GMTE oriented to obtain the minimal and compact set causal graphs of a distributed system. It is based on graph transformation approaches for the generation of three basic graphs : HBR graph, IDR graph and CAOS graph. The HBR graph presents the happened before relations of the system. The graph IDR, is the transitive reduction of the HBR graph. Then, the graph CAOS, presents the IDR graph in terms of ordered sets.

Keywords: Distributed systems, causality, happened before relation, Immediate dependency relation, causal ordred set abstraction, graphe transformation, MCSR.

Title : Context-aware services composition in cloud computing.

First registration in December 5, 2016 at The Faculty of Economics and Management of Sfax.

Abstract: Cloud computing is gaining more and more importance in the Information Technologies (IT) scope. On-demand scaling of the cloud service composition raises new challenges for delivering multi-tenancy awareness of the business process. In this thesis, we propose an approach for elastic multi-tenancy aware services composition which ensures the multi-tenant service matching and the elasticity management by handling the increase of instance number and the growing pressure during the services invocation. Indeed, the key contributions of this thesis include three phases which are: (i) MeCSM (Multi-tenant Services Composition Method) for addressing the multi-tenancy aware cloud service matching based on service pattern. The composition mechanisms are based on the multi-tenancy modes which are "native multi-tenancy" and "multiples instances", (ii) MeECSM (Elasticity of Multi-tenant Services Composition Method) which ensures the elasticity of multi-tenant composed service. An extension of the service pattern is proposed with elasticity mechanisms for the auto-scaling of the involved cloud services, (iii) MeECSM+ (Elasticity Dependency for Multi-tenant Services Composition Method) to derive elasticity dependencies between the composed service and its involved services. For that purpose, the service pattern is extended to define elasticity dependencies between the multi-tenant process and its involved services, and implies the decision of whether and how to manage service instances. The evaluation of our contributions compared to other existing approaches shows its effectiveness in implementing the elasticity of multi-tenant services composition.

Keywords: Cloud Computing, Services composition, Multi-location, Elasticity, Service pattern.

Title:

First registration in February, 2018 at The Faculty of Economics and Management of Sfax.

Abstract:

Keywords:

Title:

Defended on March 09, 2018 at The Faculty of Economics and Management of Sfax.

Abstract:

Keywords:

Title: A heuristic solution of resources provisioning for dynamic workflows

First registration in February, 2016 at The Faculty of Economics and Management of Sfax.

Abstract: In the world of software engineering, Workflow applications are a common model to describe scientific applications. To meet their execution, Workflow applications need resources. In our work, we have considered the use of resources in the Cloud which seems to be very attractive since these resources are allocated on demand and paid according to consumption.

Keywords: Cloud Computing, ressources provisionnement, dynamic Workflows, PSO algorithm.

Title: A heuristic solution of resources provisioning for dynamic workflows

First registration in February, 2016 at The Faculty of Economics and Management of Sfax.

Abstract: In this project, are interested in the software testing field, particularly the load test of Web service composition. Indeed, the test is a verification of activity which is part of the development process. Its objective is to minimize the chances of occurrences of an anomaly and designed to detect various types of possible defects. In this context, we have taken a load testing solution based on a model. We presented our approach to validate and evaluate a Web service composition of load testing solution.

Keywords: Web service composition, load testing solution.

Title: A graph transformation based approach for the validation of checkpointing algorithms

First registration in February, 2015 at The Faculty of Economics and Management of Sfax.

Abstract: This work focuses on the fault tolerance problem in distributed systems more precisely in the checkpointing technique. This technique consists of storing coherent states of the system during its execution and in case of failure, this system can restart from one of these coherent states instead of restarting from its state at time zero. The checkpointing algorithms are classified into three classes: Strictly Z-Path Free (SZPF), Z-Path Free (ZPF) and Z-Cycle Free (ZCF). Z-paths and Z-cycles are considered as undesirable patterns that can lead to incoherent states. In this context, we have developed a graph transformation based approach to validate any checkpointing algorithm by verifying its ability to detect and eliminate such patterns. Our approach has been implemented and tested using the algebraic tool "GROOVE".

Keywords: Distributed system, checkpointing algorithm, undesirable property, graphs transformation, transformation rules, validation.

Title: A formal approach for the validation of WS-CDL choreography.

Defended on March 6, 2014 at The Faculty of Economics and Management of Sfax.

Abstract: As part of the preparation of master memory, we defined a formal approach for the verification of web service choreography which is a contribution in the field of software architectures and specifically service-oriented architectures.In this context, we conducted a review on the verification of properties of web services specified in WS-CDL. At first we began by presenting choreography properties must meet for it to be correct. These properties are classified into two types: generic properties and specific properties. Generic properties can be checked on the services involved in the choreography (liveness, safety, availability and synchronization). As for specific properties, they are related to interdependence relationships between the activities of a WS-CDL process (choice, precedence and existence). For this, we have developed a tool which takes as input web services choreography and returns the result of the verification of generic properties and / or specific using the SPIN model checker. Also, we proposed a process of transformation of WS-CDL to Promela developed using XSLT.

Keywords: Choreography, WS-CDL, SPIN/Promela, XSLT.

Title: An approach for the compact and minimal representation of causality in distributed systems.

Defended on December 4, 2013 at The Higher Institute of Computer Science and Multimedia of Sfax.

Abstract: In our Master project, We have proposed an approach for the minimum and full representation of causality in a distributed system. The distributed system is viewed as a set of processes and a set of events. These processes do not share common memory or global clock and have no idea about the overall state of the system. For this, it was difficult to know the order of occurrence of events which was leading to the appearance of the concept of causality. This concept was introduced initially by Lamport defined the happened-before relation (HBR) known as a partial order to determine for a pair of events which precedes the other. One of the problems related to the HBR relation is the combinatorial explosion of the state of the system, which increases exponentially with the number of processes. Several techniques for reducing partial order have dealt with this problem. The Immediate Dependency Relation (IDR), defined by Hernandez et al as the transitive reduction of the HBR relation, is the only minimal expression of HBR. Then, in 2012, Hernandez et al have proposed a CAOS abstraction to represent causality in terms of set of events. To implement our approach, we have built the MCSR tool as a library in GMTE. It is based on graph transformation approaches for the generation of three basic graphs. The HBR graph, presents the causal dependency relations of the system. The IDR graph, which is the transitive reduction of HBR graph. The CAOS graph, presents causality in terms of event sets.

Keywords: Distributed System, Causality, Lamport, HBR, IDR, CAOS.

Title: ACME-Refinement: a new approach to describe software architectures. Defended on January 15, 2010 at the Higher Institut of Computer Science and Multimedia of Gabes.

Abstract :

Keywords:

Title : A formal approach for the verification of non-functional properties for a web service orchestrations.

Defended on July 27, 2011 at Faculty of Economics and Management of Sfax.

Abstract : The verification of web services orchestration consist of validation of generic properties such as liveness and safety and another class of properties related to interdependent relationship between activities in the BPEL process. Indeed, once the process is composed, interdependent relationship must be taken into account namely, exclusion relations, inclusion relations and prerequisite relation. In this dissertation, we present a formal approach to validate a web services orchestration specified with BPEL 2.0. This specification is translated into Promela code, the input language of SPIN model-checker to verify generic and specific properties expressed in LTL. The transformation tool of BPEL to PROMELA is achieved with the use of ANTLR.

Keywords: Web service, orchestration, BPEL, availability, interdependence properties, SPIN, ANTLR.

Title : Specification and verification of the structural and behavioural properties of Publish/Subscribe architectures.

Defended on January 31, 2009 at The Faculty of Economics and Management of Sfax.

Abstract : Publish/Subscribe system is now largely acknowledged as one of the most interesting paradigms for distributed interactions. Its main purpose is the dissemination of published events to concerned entities. This dissemination must be achieved by taking into account structural and behavioural constraints. In this work, we extend P/S-CoM, as a formal approach supporting the correct modelling of Publish/Subscribe architectural style with respect to structural properties. We consider the behavioural properties, which are related to event dissemination and have to be respected during the lifetime system. Published events have to be spread to concerned entities explicitly with neither duplication nor loss and with respect to their publication order. We propose using the automata with multiplicities as a formalism for specification. This tool will be used here to ensure that the system is evolving correctly with respect to its architectural style. In fact, configuration catches are represented as automata with multiplicities, which will be translated into Promela, the input language of the SPIN model checker in order to verify structural and behavioural properties expressed in LTL.

Keywords: Correctness; Publish/Subscribe; architectural stylebehavioural properties; automata with multiplicities; SPIN.

Title : Sensor Networks and Population Protocols: Application of the diffusion and improved with the rendezvous model.

Defended on January 9, 2010 at The Faculty of Economics and Management of Sfax.

Abstract : Wireless sensor networks are a new generation of networks that need specific models and algorithms. We are interested specifically in mobile wireless sensor networks that are considered as anonymous asynchronous distributed mobile systems. As broadcast is one of the most important applications for such networks, and as it depends on the communication model, we tried to find the most suitable one to make a distributed broadcast algorithm. We adopted the population protocols, the Angluin's model of pairwise interactions of anonymous finite-state agents, to broadcast an information. We tried to modify this model to avoid the information duplication and then calculated the complexity of the algorithm. Then, we extended the model with the rendezvous one that made the stabilization of the algorithm faster. The implementation, the simulation, and the validation of these algorithms and results have been done with Visidia.

Keywords: anonymous mobile sensor network; broadcast; distributed probabilistic algorithm; population protocols; rendezvous