MTA4ESC is a scaling middleware which is both multi-tenancy awareness and workload-adaptive allowing services providers to perform more efficient multi-tenant services composition and managing their elasticity. It considers the cost savings limitations of such compositions under workloads variation which affects the pay as-you-go model of the cloud resources. The MTA4ESC consists of three basic modules which are (i) cloud services composition which ensures the multi-tenant services matching based multi-tenancy modes where single instance of a process serves multiple tenants, (ii) elasticity management of the involved services that may result from the workload variation and, (iii) elasticity dependency controller for analyzing elasticity dependencies between the multi-tenant business process and its involved services.

MCSR (Minimal Causal and Set Representation) tool constructs, for a distributed computation, the minimal causal graph (IDR graph) at a single event level and a causal consistent compact graph (CAOS graph) at an event set level. For this, we use the Immediate Dependency Relation (IDR) and the Causal Order Set Abstraction (CAOS), respectively. Both resultant causal graphs drastically reduce the state-space of a system. The MCSR approach begins receiving a database of Vector Clocks as input, from which the fully-causal HBR original graph is generated. Then, by using graph transformation rules, the IDR and the CAOS graphs are generated. Two sets of rules are proposed: the "HBR2IDR" for the generation of the IDR graph and the "IDR2CAOS" for the generation of the CAOS graph.

CDLVT is a formal approach of verifying non-functional properties for web services choreographies. Two classes of properties have to be taken into account: global and internal properties. Global properties can be verified for any web service involved in a given choreography. Internal properties are the dependent relations between activities for a given WS-CDL specification. To do this, we have developed a tool which takes a web service choreography specified with WS-CDL as an input and a set of properties and returns the verification result as an output. The verification is achieved by using the SPIN model-checker.

BPELVT is a formal approach to validate web services orchestrations. Two classes of properties have to be taken into account: generic and specific properties. Generic properties can be verified for any web service involved in a given orchestration. Specific properties are the dependent relations between activities for a given orchestration process. To do this, we have developed a tool which takes a web service orchestration specified with BPEL 2.0 as an input and a set of properties and returns the verification result as an output. The verification process is achieved with the SPIN model-checker. The transformation from BPEL to Promela, the input language for SPIN, is fullfilled with the use of ANTLR tool (ANother Tool for Language Recognition).

The structures studied in the context of my PhD research as the concept of semi-ring, module, automata with multiplicities and other combinatorial structures can be manipulated in the MuPAD language using the library . MuPAD-Combinat is an open system of algebraic combinatory. It currently contains functions that deal with the usual combinatorial classes (partitions, tables and decomposable classe), Schubert polynomials, the symmetric group and weighted automata. It provides the user with tools to build new classes and combinatorial algebras. Its development has started since spring 2001 and officially incorporated in the MuPAD library since version 2.5.0. The library MuPAD-Combinat offers many features of algebraic combinatory. The package WeightedAutomaton of the MuPAD-Combinat library contains a set of procedures for manipulating automata with multiplicities. To build an automaton using this package, you must provide the dimension of this automaton (number of states), the alphabet A, the input vector, the transition matrices for each letter of the alphabet and the output vector.