Keywords: Cloud Computing, Multi-Clouds, Open Cloud Computing Interface (OCCI), Model-Driven Engineering (MDE), Reverse-Engineering, Google Cloud Platform (GCP), Formal Methods, Formal Verification, Alloy, Interoperability viii Nuage informatique, Multi-nuages, Open Cloud Computing Interface (OCCI), Ingénierie dirigée par les modèles (IDM), Rétro-ingénierie, Google Cloud Platform (GCP), Méthodes formelles, Vérification formelle, Alloy, Interopérabilité

In recent years, multi-cloud computing which aims to combine different offerings or migrate applications between different cloud providers, has become a major trend. Multi-clouds improve the performance and costs of cloud applications, and ensure their resiliency in case of outages. But with the advent of cloud computing, different cloud providers with heterogeneous cloud services (compute, storage, network, applications, etc.) and Application Programming Interfaces (APIs) have emerged. This heterogeneity complicates the implementation of an interoperable multi-cloud system. Several multi-cloud interoperability solutions have been developed to address this challenge. Among these solutions, Model-Driven Engineering (MDE) has proven to be quite advantageous and is the mostly adopted methodology to rise in abstraction and mask the heterogeneity of the cloud. However, most of the existing MDE solutions for the cloud remain focused on only designing the cloud without automating the deployment and management aspects, and do not cover all cloud services. Moreover, MDE solutions are not always representative of the cloud APIs and lack of formalization.

To address these shortcomings, I present in this thesis an approach based on Open Cloud Computing Interface (OCCI) standard, MDE and formal methods. OCCI is the only community-based and open recommendation standard that describes every kind of cloud resources. MDE is used to design, validate, generate and supervise cloud resources. Formal methods are used to effectively reason on the structure and behaviour of the encoded cloud resources, by using a model checker verifying their properties. This research takes place in the context of the OCCIware project, which provides OCCIware Studio, the first model-driven tool chain for OCCI. It is coupled with OCCIware Runtime, the first generic runtime for OCCI artifacts targeting all the cloud service models (IaaS, PaaS, and SaaS).

In this dissertation, I provide two major contributions implemented on top of the OCCIware approach. First, I propose an approach based on reverse-engineering to extract knowledge from the ambiguous textual documentation of cloud APIs and to enhance its representation using MDE techniques. This approach is applied to Google Cloud Platform (GCP), where I provide GCP Model, a precise modeldriven specification for GCP. GCP Model is automatically inferred from GCP textual documentation, conforms to the OCCIware Metamodel and is implemented within OCCIware Studio. It allows one to perform qualitative and quantitative analysis of the GCP documentation. Second, I propose in particular the fclouds framework to achieve semantic interoperability in multi-clouds, i.e., to identify the common concepts between cloud APIs and to reason over them. The fclouds language is a formalization of OCCI concepts and operational semantics in Alloy formal specification language. To demonstrate the effectiveness of the fclouds language, I formally specify thirteen case studies and verify their properties. Then, thanks to formal transformation rules and equivalence properties, I draw a precise alignment between my case studies, which promotes semantic interoperability in multi-clouds.

PhD is the biggest achievement but also the most challenging experience in my life, so far. Therefore, I would like to express my utmost gratitude to the people who helped me during this journey.

Foremost, I am truly grateful to my supervisor, Philippe Merle for many reasons. Thank you for taking my application for this thesis into consideration three years ago and for believing that I am a perfect fit for the job since our very first interview. Thank you for your guidance, which taught me the ropes of research, and for plenty of brilliant ideas, which were an inspiration for me. Thank you for helping me hone my skills and pushing me forward to be the best version of myself. I was determined to succeed to be worthy of the trust you placed in me. Our relationship made of taste for research, professionalism and kindness meant a lot to me. I highly admire your passion for your work, and I sincerely believe that you are an excellent researcher and a genuine person. And as I told you once before, I could not have imagined having a better mentor during my PhD. Thank you from the depths of my heart! Next, I would like to thank the members of my thesis committee for devoting their time to read the manuscript and for their constructive feedback. Benoit Combemale and Christian Perez, thank you for accepting to review my manuscript. I would also like to thank Hélène Coullon for accepting to be part of my committee and Laetitia Jourdan for accepting to chair it.

Further gratitude is due to the members of the Spirals team at Inria research center, who I met since October 2015. Actually, during the last three years, I had the chance to be part of Spirals and it was a pleasure meeting many wonderful people there. Everyone was friendly and open for discussions, which made my stay extremely pleasant. I sincerely thank the team leader, Lionel Seinturier, for his effective direction, for providing a very motivating environment for preparing PhDs and for empowering my ambitions and helping me achieving them. I acknowledge your support and the support of Laurence Duchien when I came to you with my proposition to apply for the L'Oréal-UNESCO For Women In Science award. Also, thanks to Laurence for being a role model for many young female researchers like me and for your sincere advises for my career. I will always remember them. I would like to thank Walter Rudametkin, not only for your insightful comments, but also for your everyday friendship, for giving me access to your precious media server and for going out and drinking beers together. Besides, thank you and Marcia for receiving me in "Chez Rudametkin" and for those unforgettable tacos. I confirm that the 5 star on Google is well-deserved! ;) I salute Clément Quinton for his ambition and love of life. I enjoyed swimming with you on Fridays. Thank you as well for sharing with me your experience of becoming an associate professor. My warm wishes to you and your beautiful family. Thanks to Simon Bliudze with whom I shared the office for the last year. Thanks for working late so often, it helped me keeping focused and feeling well-surrounded. :) Also, thanks for giving me valuable feedback and propositions regarding my work, at each time I asked you. I hope we will work together sometime soon since many ideas emerged from these inspiring discussions. I would also like to thank my two former office mates, Christophe Gourdin and Gustavo Sousa. Thanks to Christophe for teaching me some "Chti" vi language and for technical support when I started the implementation work in the OCCIware project. Here's to the prosperity of your startup! Thanks to Gustavo for the tips and recommendations when I first arrived to Lille and for the enriching conversations in the initial stage of my PhD. You were the first friend I made in the team and in Lille in general. Big thanks to Faiez Zalila for attending and efficiently participating to the weekly meeting with Philippe and me and for being the technical leader in the OCCIware project. I acknowledge your assistance with the modeling techniques, which allowed me to go further with my contributions. I would like to mention Yahya Al-Dhuraibi who started his PhD at the same time as me and under the supervision of Philippe too. I shared good moments with you when we attended the conference in Madeira and I admire your kindness, modesty and generosity. I wish you all the best for your future, you deserve it! Thanks to Maxime Colmant for helping me preparing my courses when I started teaching at the University of Lille.

I thank the OCCIware French project and the "Hauts-de-France" regional council for providing scholarships and appropriate facilities to pursue my doctoral studies. I also thank L'Oréal foundation for awarding me and providing research grants.

Thanks to my friends in Lille, Tonie and Jad. Tonie, I am so happy that I met you. I've always had fun with you and I really enjoyed our little tradition of Saturday lunch, although I missed some Saturdays because I needed to work. Jad, it was great news for me when I knew that you will be preparing a PhD also at the University of Lille, after we graduated together from the Antonine University. Thanks for the "Reeflex" evenings, for bringing me souvenirs when you visited a new city and for the catch up over coffee when you were at Inria. Who knows, maybe we will be colleagues again one more time! Thanks to my cousin Yara and to my friends in Lebanon, Alain, Alfred, Chantal and Rami for always being there through WhatsApp, for your sense of humor and for the amazing outings at each time I visited Lebanon. You boosted my energy to reach this end.

I spare a moved thought for my guardian angel, my grandmother Farida who raised me during my early childhood and who left years ago. I wish that you were here with me and I hope that you are proud of me.

Big thanks to my dear parents, Joseph and Rita, who gave me the best of education and trusted my plan when I decided to move to France. Even from far away, I always felt your support. Dad, you taught me to aim high and I would not be who I am today without you. Mum, you are a perfect example of devotion and strength, I learn from you a lot and on daily basis.

Last but not least, I want to thank with great affection, my handsome fiancé, Benjamin Danglot, for being my backbone and my everyday bundle of happiness for the last two years. You suffered with me the side effects of preparing a thesis. Thank you for everything you do to help my dreams come true and for loving me unconditionally. I feel so lucky to have you by my side "habibi".

IV Contributions 93

Chapter 1

Introduction

Contents C loud computing, which is gaining the attention of both academia and industry for the last decade, was not born from scratch but is a normal evolution of many domains such as distributed computing, grid computing and service-oriented computing. Many computing researchers and practitioners have attempted to define cloud computing in various ways. I give below the most commonly used definitions:

• "A Cloud is a type of parallel and distributed system consisting of a collection of inter-connected and virtualized computers that are dynamically provisioned and presented as one or more unified computing resource(s) based on servicelevel agreements established through negotiation between the service provider and consumers." [START_REF] Buyya | [END_REF]].

• "Cloud computing refers to both the applications delivered as services over the Internet and the hardware and systems software in the data centers that provide those services." [START_REF] Armbrust | [END_REF]].

• "Cloud computing is a model for enabling ubiquitous, convenient, on-demand network access to a shared pool of configurable computing resources (e.g., networks, servers, storage, applications and services) that can be rapidly provisioned and released with minimal management effort or service provider interaction." [START_REF] Mell | The NIST Definition of Cloud Computing[END_REF]].

To summarize, cloud computing enables computing resources, software, or data to be delivered as a service and on-demand through the Internet, so these resources have become cheaper, more powerful and more available than ever before.

More precisely, cloud computing is a model composed of three deployment models, three service models and three delivery models.

Deployment models. Cloud environments can have different access types, that are called deployment models. The latter can be private, public or hybrid. Private cloud environments are owned by a single organization and they can be built by relying on technologies like OpenStack [opea], whereas public cloud environments are owned by a third-party cloud provider such as Amazon Web Services (AWS) and Google Cloud Platform (GCP). Usually, a cloud developer requires using private clouds for testing a cloud application, then migrating to public clouds so the application can be publicly accessed by cloud users. And sometimes, the cloud developer requires using a hybrid cloud, i.e., that comprises public and private cloud environments. It allows the cloud developer to make his/her application publicly accessed by hosting its Web server on a public cloud, and to privately store sensitive data by keeping his/her application database in a private cloud.

Service models. Cloud providers offer functionalities as services at different layers of the cloud stack, i.e., service models: Infrastructure-as-a-Service (IaaS), Platform-as-a-Service (PaaS) and Software-as-a-Service (SaaS).

• IaaS : where the capability provided to the IaaS user is to provision virtual machines and to configure the infrastructure concerns: processing, storage, networking, and other computing resources.

• PaaS : where the capability provided to the PaaS user is to deploy an application and it is limited to the database(s), application server(s), compilation tools, libraries, etc.

• SaaS : where the capability provided to the SaaS user is to manage applications running on a cloud Infrastructure and/or Platform, and accessible through a web browser. A SaaS should rely on the principle of multi-tenancy, where multiple independent instances of one or multiple applications operate in a shared environment.

Delivery models. Cloud resources can be provisioned from either a single cloud or multiple clouds. This is known as the delivery model. In this section, I describe each of the existing delivery models and I highlight the advantages of a multi-cloud delivery model, which interests us in this dissertation.

• Single cloud : where cloud applications are limited to be deployed on a single cloud among others, i.e., to benefit from services of only one cloud provider at a time.

However, several cloud outages have taken place in the past [START_REF] Ko | [END_REF]], which prove that the sentence "do not place all your eggs in one basket" is equally applicable to the cloud ecosystem. Therefore, some cloud application may require to exploit services from multiple cloud environments, at the infrastructure, platform, and software layers. In this case, the cloud developer should perfectly manage to deal with dependencies and to ensure separation of concerns. As Petcu explained in [Petcu 2013], there are two basic delivery models in multiple cloud systems: Federated Clouds and Multi-Clouds. Petcu has drawn a clear positioning of multi-clouds versus other cloud models. I summarize it as follows:

• Federated clouds: where the cloud providers are in agreement with each others to enhance the service offered to their consumers, e.g., European Grid Infrastructure Federated Clouds (EGI FC) which is a federation of private clouds.

• Multi-clouds: where the application provisions multiple cloud varying services, without a prior agreement with and between the cloud providers, but with a third party building a unique entry point for multiple clouds. This strategy has been adopted in the cloud computing industry since a while in order to improve disaster recovery and geo-presence, to use unique cloud services from different providers as they are needed, and to ensure unlimited scalability of cloud applications, as explained in [Petcu 2013].

The remainder of this introductory chapter is organized as follows. Section 1.1 presents the context of this thesis. In Section 1.2, I identify the problems that motivate this research. Section 1.3 introduces the research questions that this dissertation aims to answer. Next, in Section 1.4, I present the main goals of this thesis. Section 1.5 presents the vision of my research. Section 1.6 introduces my proposed solution. In Section 1.7, I summarize the structure of this dissertation. Finally, in Section 1.8, I detail the publications derived from my research.

Thesis Context

This thesis is supported by both the OCCIware [occc] research and development project funded by the French Programme d'Investissements d'Avenir (PIA), and the Hauts-de-France Regional Council. The OCCIware project promotes the OCCI standard to address the lack of unified cloud computing standard and facilitate the development of services. Therefore, the works carried on in this thesis are built on the OCCI standard by using the OCCIware approach.

This thesis is produced in the Spirals team. Spirals is a joint project-team between Inria Lille-Nord Europe research center and the University of Lille. Spirals currently consists of eight permanent members and about twenty-five nonpermanent members. The research areas of Spirals are distributed systems and software engineering. The research areas of this thesis are particularly multi-cloud computing, Model Driven Engineering (MDE) and formal methods.

Problem Statement

Due to the emergence of numerous cloud providers and their heterogeneity, provisioning cloud services is not a straightforward task. I state the main problem addressed by this dissertation as follows:

The cloud shows several favorable features like elasticity and pay-as-you-go. In order to take advantage of these features, the cloud computing market counts today variety of cloud providers like Amazon, Google, Microsoft, etc. Cloud providers offer varying infrastructure, platform or software services. Even at the same service layer, cloud providers use heterogeneous terms, concepts, and features, which usually are not aligned with those of competing providers. These semantic differences are critical in cloud computing as they make migrating an application across providers a very complicated and costly task. In addition, cloud providers give access to their resources through heterogeneous Cloud Resource Management (CRM)-Application Programming Interface (API)s. The management of a potentially large number of cloud services with heterogeneous CRM-APIs is a challenge, because of incompatibility between the different APIs. Worse still, the semantics of these CRM-APIs is informally described in English prose in their documentation available at the provider's website. Therefore, it is usually impossible to understand the behaviour of a cloud when the developer requests a virtual machine for example. For the above concerns, the dependency to a single cloud provider is promoted, the multi-cloud environment is prevented and the migration from one cloud to another becomes a very complicated task. The comic strip in Figure 1.1 illustrates the problem above, i.e., the heterogeneity in a multi-cloud context that leads to a lack of interoperability across providers. I credit the work for designing the amazing comics of my thesis to Olivier Audy.

More specifically, cloud stakeholders face the following challenges.

Heterogeneous service models. Cloud providers offer different services that belong to the Infrastructure (IaaS), Platform (PaaS) or Software (SaaS) layers. We use the abbreviation Everything as a Service (XaaS) to refer to all categories. These categories consist in the "Service Model". Service models contain highly heterogeneous cloud resources, which make difficult the overall management of a computer system from infrastructure to application resources.

Heterogeneous CRM-APIs. Cloud services are often exposed as Web services, which follow the industry standards such as Web Services Description Language (WSDL)1 , Simple Object Access Protocol (SOAP) 2 and Universal Description, Discovery and Integration (UDDI)3 [START_REF] Paraiso | A Federated Multi-Cloud PaaS Infrastructure[END_REF]]. They frequently rely on REpresentational State Transfer (REST)ful [Fielding 2000] APIs that provide programmatic access to the resources offered by a cloud provider through Create, Retrieve, Update and Delete (CRUD) operations. For example, the Amazon cloud services are accessible via a SOAP API, whereas other clouds are based on a REST API, which leads to an incompatibility between these two different APIs.

Semantic differences. The semantics refers to the description of a cloud service by its provider. These descriptions are heterogeneous because a cloud provider employs concepts, which usually do not directly map to those of a competing provider. In fact, even if cloud providers offer the same service, the latter may have different names, characteristics and functionalities. For instance, GCP refers to its compute service as "instance", whereas DigitalOcean calls it "droplet". These semantic differences are critical in cloud computing as they make migrating an application across providers a very complicated and costly task.

Lack of verification. Cloud solutions provide services, libraries or modeldriven tools to provision cloud resources. However, once provisioned, the deploy-ment of the applications can face several problems such as misconfiguration of links between resources, lack of resources on the hosts in which the applications are deployed, human errors, etc. The only way to be sure that the cloud configurations will run or fail is to deploy them on the target executing environment. Moreover, there is no way to verify that deployed configurations are conform with those desired. The lack of verification tool becomes quickly painful and expensive when the deployment task is repeated several times.

Lack of formalization. The semantics of cloud APIs is informally described in their documentation available at provider websites within English prose. It is then difficult to understand the behaviour of a cloud when the developer requests a virtual machine for example. Moreover, the cloud solutions are numerous and also lack of precise documentation, which complicate their understanding and comparison. This lack of formalization hinders the understanding of the cloud APIs and solutions, thus complicates the provisioning process and also misleads the alignment and comparison between cloud offerings.

Vendor lock-in. It is recognized as one of the greatest challenges to cloud adoption where cloud clients are locked-in to a specific cloud provider due to the heterogeneity. Therefore, vendor lock-in is a serious result of all the problems that I discussed above. This problem hinders the complete exploitation of the full capabilities of cloud computing since it prevents two main intended aspects: portability and interoperability, which are closely related terms and may often be confused. Cloud interoperability is the integration between several cloud offerings, whereas portability is the ability to move applications between different cloud providers. Cohen clarifies in [Cohen 2009] the similarities and the differences among these terms in an attempt to exemplify and differentiate them.

The work presented in this thesis aims to alleviate the challenges presented above.

Research Questions

More specifically, this thesis aims to answer the following three research questions (RQs):

• RQ#1: Is it possible to have a solution that allows to represent all kinds of cloud resources despite their heterogeneity, and a complete framework for managing them?

Chapter 1. Introduction -How to design the cloud developer needs at a high-level of abstraction? -How to verify the cloud structural and behavioral properties before any concrete deployments?

-How to deploy and manage cloud configurations?

• RQ#2: Is it possible to automatically extract precise models from cloud APIs and to synchronize them with the cloud evolution?

-How to provide an accurate description for a cloud API?

-How to correct the existing drawbacks in a cloud API documentation?

-How to analyze a cloud API documentation?

• RQ#3: Is it possible to reason on cloud APIs and identify their similarities and differences?

-How to better understand cloud solutions?

-How to make sure that a cloud solution reflects the desired behaviour?

-How to ensure an accurate migration from a cloud solution to another?

These research questions are explored in next sections.

Thesis Goals

The objective of this thesis topic was to propose the first formal framework to rigorously handle cloud resources. This framework allows to model, analyze, design, deploy, manage every kind of cloud resources, and to reason over them. This framework is based on the Open Cloud Computing Interface (OCCI) [Edmonds 2012, occa] of the Open Grid Forum (OGF) recommendation. The tooling of this framework relies on MDE techniques, particularly the Eclipse Modeling Framework (EMF) and the Models@run.time approach. The formalization of this framework relies on formal specification languages such as the Alloy [Jackson 2012] language developed by Professor Daniel Jackson from the Massachusetts Institute of Technology (MIT). To achieve this objective, I decompose it into the following goals.

Regarding RQ#1, this thesis aims to provide mechanisms to interact with heterogeneous cloud environments. These mechanisms allow one to model, analyze, design, deploy and manage every kind of cloud resources.

Regarding RQ#2, this thesis aims to propose mechanisms to automatically build a cloud model from the corresponding cloud API. These mechanisms rely on reverseengineering techniques. They consist in extracting knowledge from a cloud API 1.5. Thesis Vision documentation in order to infer the concepts to be defined in the cloud model so it correctly reflects the real cloud API. Also, these mechanisms allow to automatically update the cloud model in case changes occurred to the cloud API.

Regarding RQ#3, this thesis intends to provide mechanisms to draw a precise alignment between cloud APIs. For such purpose, I exploit formal languages to rigorously and precisely encode cloud concepts and operations and to reason over them.

Thesis Vision

We discussed earlier in this chapter that cloud computing encompasses heterogeneous cloud providers. As illustrated in Figure 1.2, this thesis takes advantage of model-based and formal approaches in order to rise in abstraction from the heterogeneous real-world and promote multi-cloud computing. The approaches presented in this thesis are represented in blue. The OCCIware model-driven approach is discussed in the background part of this thesis, and the fclouds formal approach is discussed in the contributions part of this thesis. More precisely, this thesis aims at inferring models from multi-clouds using the OCCIware platform, and then formally reasoning on these models using the fclouds framework.

Model-Driven

Proposed Solution

In this section, I provide an overview of the contributions described in this dissertation. As stated before, the goal of my thesis is to provide approaches, languages, tools for inferring and enhancing the knowledge of cloud APIs, precisely representing this knowledge and efficiently reasoning over it. The main contributions of our work are summarized as follows:

Precise models for cloud APIs. My first contribution is to enhance the knowledge representation in cloud APIs by automatically inferring a precise model from the cloud textual documentation. My approach is applied on a major cloud provider, GCP. To address the drawbacks of GCP textual documentation, I propose a precise model that describes GCP API. It consists in a precise specification that describes without ambiguity the knowledge and activities in GCP to avoid confusion and misunderstandings. This model-driven specification, called GCP Model, is automatically inferred from the textual documentation of GCP. GCP Model conforms to the OCCIware Metamodel and is implemented within the open source model-driven Eclipse-based OCCIware tool chain. Thanks to our GCP Model, I offer corrections to the drawbacks I identified in GCP textual documentation. Also, I analyze GCP by drawing conclusions regarding their documentation and quantifying their services.

The fclouds framework. I provide as second contribution fclouds, the first formal framework for semantic interoperability between cloud APIs. By semantic interoperability I mean to identify the similarities and differences between cloud APIs concepts and to mathematically reason over them. fclouds contains a catalog of cloud APIs that are precisely described. It will help the cloud customer to understand the behaviour of the cloud API but also how to migrate from one API to another, thus to promote semantic interoperability. To implement the formal language that will encode all the APIs of our fclouds framework, I advocate the use of formal methods, i.e., techniques based on mathematical notations. They will allow us to rigorously encode cloud concepts and behaviour, validate cloud properties and finally define formal transformation rules between cloud concepts. I adopt the concepts of the OCCI common standard to define the formal language of the fclouds framework. I choose to formalize OCCI with Alloy [Jackson 2012], a lightweight promising formal specification language designed by Daniel Jackson from the MIT. This dissertation is divided in five parts and six chapters, as shown in Figure 1.4. While this introductory chapter is part of the first part, the second one encloses the State of the Art. In the third part, I present OCCIware, which is the model-driven environment on which I rely to implement my works. The fourth part presents the two contributions of this dissertation. Finally, the last part includes the conclusions and perspectives of this dissertation. Below, I present an overview of the chapters that compose the different parts.

Dissertation Roadmap

Part II: State of the Art Chapter 2: Model-Driven Approaches for the Cloud In this chapter, I present the approaches that are used in order to ensure multi-clouds, namely standards, services, libraries and models. I focus on model-based cloud solutions and I propose a taxonomy to provide a better understanding of the concerns in which our work takes place. I list and describe the most relevant related works in terms of our taxonomy criteria. Since our work presents a solution for multi-clouds, the idea of this chapter is to explore the existing solutions and their limitations.

Part III: Background Chapter 3: Modeling, Verifying, Generating and Managing Cloud Resources with OCCIware. In this chapter, I present OCCIware, the project that supports this thesis and the paltform that I used to implement my contributions.

OCCIware proposes to textually and graphically encode cloud APIs and cloud configurations via OCCIware Studio. The latter is a model-driven environment for OCCI standard, based on an Ecore metamodel. Then, OCCIware Studio is linked with OCCIware Runtime, an execution environment for OCCI artifacts. Therefore, from a designed and verified OCCI configuration, we can generate a deployment script via the CURL Generator tool. Later, these configurations can be managed at runtime via generated connectors deployed on OCCIware Runtime.

Part IV: Contributions

Chapter 4: Inferring Precise Models from Cloud APIs Textual Documentations. In this chapter, I present my approach for retrieving information from cloud APIs, improving their representation and discovering new knowledge from them. This approach is experimented by studying the textual documentation of GCP, one of the leaders in the cloud market. Then, I build a precise model for GCP, called the GCP Model. Thanks to this model, I study GCP API and provide corrections to the six drawbacks of its current informal documentation.

Chapter 5: Specifying Heterogeneous Cloud Resources and Reasoning over them with fclouds. In this chapter, I present my approach for formally specifying cloud APIs, called the fclouds framework. Based on Alloy formal language and the OCCI standard, I define a formal language for cloud computing that relies on first-order logic paradigm combined with relational algebra. Then, I show how having formal specifications of cloud solutions allow to check their behaviour, Chapter 1. Introduction detect their inconsistencies, and remove their ambiguity to understand their similarities and promote their interoperability.

Part V: Conclusion

Chapter 6: Conclusions and Perspectives. In this chapter, I conclude the work presented in this dissertation. I discuss some limitations that motivate new ideas and future directions as short-term and long-term perspectives.

Publications

The contributions derived from this thesis have been published in international peer-review conferences. In this section, I detail all the publications resulted from my research for the last three years. These publications are ordered by year of publication.

International Conferences

International Journal

In addition, one journal article is under submission:

• Faiez Zalila, Stéphanie Challita, and Philippe Merle. "Model-Driven Cloud Resource Management with OCCIware." Future Generation Computer Systems (FGCS), 2018 [Zalila 2018] (Impact factor 4.639).

Awards

During this thesis, I was selected as an ambassador of the French fellowship L'ORÉAL-UNESCO FOR WOMEN IN SCIENCE 2018. Among 900 applications, 20 female PhD candidates and 10 female postdocs were granted this award. Also, I received two student travel grants from:

• IEEE CLOUD 2017 conference that took place in Honolulu, Hawaii, USA, and,

• FormaliSE 2018 conference (co-located with International Conferences on Software Engineering (ICSE)) that took place in Gothenburg, Sweden.

T oday, the plethora of cloud providers and their heterogeneity hinder their in- teroperability. Therefore, many solutions have emerged to add abstraction between the cloud providers and provide mechanisms to automate the provisioning of services from multi-clouds. Among these solutions, MDE has received a significant attention in the development of software for cloud computing. MDE is a software development methodology that allows software developers to design the software concerns at a high level of abstraction, hide different implementation details, reduce complexity, ease reuse, and thus improve software quality. Since 2010, several MDE approaches for the cloud have emerged. However, each one targeted a particular problem and resolved it within an ad-hoc manner. In fact, some years after the emergence of the cloud computing, several works [START_REF] Bruneliere | [END_REF][START_REF] Baryannis | [END_REF] were interested to the synergy between the cloud and MDE. However, no work gave a consensus on the set of models, languages, model transformations and software processes for the model-driven development of the cloud applications. In this chapter, I present the first detailed study about the use of MDE for the cloud.

Chapter 2. Model-Driven Approaches for the Cloud

This chapter is structured as follows. Section 2.1 recalls the concept of "Cloudware engineering" and classifies the existing Cloudware engineering solutions into three categories that I call spaces. Section 2.2 describes a taxonomy for explaining Model-Driven Approaches for the Cloud (MDAC). Therefore, I list the different identified usages for MDAC, during the different phases of building an application for/in the cloud. Afterwards, I discuss what an eventual MDAC can contain as concepts to reply to the different usages needs. Then, I discuss how these concepts can be encoded and what are the different possible approaches to do that. Section 2.3 details twenty-two existing MDAC. Then, I discuss these solutions according to my taxonomy criteria. Section 2.4 identifies some limitations in the existing approaches. Finally, Section 2.5 concludes the chapter.

Multi-Cloud Ecosystem

The emergence of the virtualization and the cloud computing has fostered the deployment of the software on the cloud. This specific kind of software is called Cloudware. The Cloudware engineering requires us to update the classical software engineering approaches to be adapted to the cloud computing specificities such as elasticity and portability. To promote interoperability between clouds, i.e., to enable multi-clouds, the Cloudware engineering market counts numerous solutions at different levels of abstraction, traditionally called service layers. From my point of view, these solutions can be classified into three spaces, as shown in Figure 2.1. I identify the Provider Space that offers solutions for the cloud provider, the Programming Space that offers solutions for the cloud developer and the Modeling Space for the cloud architect. Multi-cloud solutions, whether they belong the Provider Space, Programming Space or Modeling Space, follow sometimes the current emerging cloud standards.

Standards. Cloud standards result from collective agreements and aim at providing some concepts, characteristics and implementations to be commonly used by cloud providers. Among cloud standards, I identify:

• Cloud Application Management for Platforms (CAMP) [Carlson 2012, cam]:

the Organization for the Advancement of Structured Information Standards (OASIS)'s CAMP standard targets the deployment of cloud applications on top of PaaS resources.

• Cloud Data Management Interface (CDMI) [cdm]: defines a RESTful interface that allows cloud applications and users to retrieve and perform operations on the data from the cloud. • Cloud Infrastructure Management Interface (CIMI) [START_REF] Davis | [END_REF]]: the Distributed Management Task Force (DMTF)'s CIMI standard defines a RESTful API for managing IaaS resources only.

• OCCI [Edmonds 2012, occa]: the OGF's OCCI proposes a generic resourceoriented model for describing and managing any kind of cloud resources, including IaaS, PaaS, and SaaS.

• Open Virtualization Format (OVF) [ovf]: the DMTF's OVF standard defines a packaging format for portable virtual machine images.

• Topology and Orchestration Specification for Cloud Applications (TOSCA) [START_REF] Binz | [END_REF]]: the OASIS's TOSCA defines a model to describe and package cloud application artifacts and to deploy them on IaaS and PaaS resources.

Discussion

Using standards for cloud computing is quite advantageous because they result of a collective agreement and they extract the key actions and characteristics of cloud providers. Also, being a standard means that several implementations have been successfully built using this standard. However, standards are usually specific for a particular cloud service model. Moreover, leading cloud providers have unfortunately no interest in adopting a standard API like the one offered by OCCI to ease interoperability with other clouds. Each of the cloud providers would rather have proprietary, closed source implementations with custom APIs. However, OCCI has proven its utility in several contexts. For example, the EGI FC [egi] is based on OCCI to ensure interoperability among twenty cloud providers and over three hundred data centers. Furthermore, OCCI attracts several cloud brokers such as CompatibleOne [START_REF] Yangui | [END_REF]] that aims at ensuring seamless access to the heterogeneous resources of cloud providers. For these reasons among others, I propose in this thesis an OCCI-based approach for interoperability in a multi-cloud context.

In the following, I present the Cloudware spaces and highlight the problem at each space of the cloud ecosystem.

Provider Space

The cloud market counts today a plethora of cloud providers that, as shown in Table 2.1, are heterogeneous in terms of their deployment model, service model and management interface. This heterogeneity leads to vendor lock-in. Services. To address the providers' heterogeneity problem, the solution in this space would be a service that offers a unique interface to handle the heterogeneity of different APIs. A service is expected to intermediate the relationship between the cloud providers and users to simplify the process of combining multiple cloud services. In this subsection, I survey different cloud services, whether they are commercial or open source.

• Aeolus [aeo]: is an open source European research project aiming at automating the deployment and reconfiguration of machine pools in the clouds.

• Aneka [START_REF] Vecchiola | [END_REF]]: is a PaaS, that is commercialized by Manjrasoft [man], for building .NET applications and deploying them on either public or private clouds.

• CompatibleOne [START_REF] Yangui | [END_REF]: is an open source PaaS to automate application deployment on multiple providers. It is based on CDMI and OCCI standards.

• Kaavo [kaa]: is a commercial management interface for configuring and managing applications on the supported cloud providers and platforms.

• mOSAIC [mos, Sandru 2012]: is a European project that offers an open source API for the development and deployment of applications that use multiple clouds.

• Optimis [START_REF] Ferrer | [END_REF]]: is also a European project that offers an open source PaaS that allows cloud service provisioning and the management of the lifecycle of the services.

• RightScale [rig]: is a commercial service for deploying and managing applications across clouds.

• Scalr [scab]: similar to RightScale, Scalr provides deployment of virtual machines in various clouds and includes automated triggers to scale up and down.

• STRATOS [START_REF] Pawluk | [END_REF]]: offers single sign-on and monitors resource consumption and the fulfillment of service level agreements and offers autoscaling mechanisms.

Discussion

A cloud service only masks the heterogeneity problem and does not semantically resolve it. Cloud users would not have a way to understand how their applications and sensitive data are dealt with inside a cloud, thus hampering trust to cloud services. Also, an important limitation in using cloud brokering services is the user reliance on the broker to be continuously up to date with new cloud technologies, options and offerings.

Programming Space

In order to allow developers to provision cloud services, each cloud offers one or several language-specific Software Development Kit (SDK)s to hide technical details of APIs. However, these SDKs are heterogeneous. Therefore, many multi-cloud libraries have emerged to allow developers to add abstraction between the cloud SDKs and enable multi-clouds. In this subsection, I survey different multi-cloud libraries providing a uniform way to access multiple services and resources, as well as facilitating the provisioning of services and resources from multiple clouds.

• Fog [fog]: is a Ruby library that provides an interface, making clouds easier to work with and to switch between providers.

• Gophercloud [gop]: is a Go library that allows cloud developers to connect to their applications on OpenStack clouds.

• jclouds [jcl]: is a Java library that introduces abstractions aiming the portability of applications and supports more than thirty cloud providers.

• libcloud [lib]: is a Python library that controls Virtual Machine (VM)s from different cloud providers.

• SimpleCloud [sim]: is a PHP library for accessing storage, queue and database services in the cloud.

Discussion

The multi-cloud libraries are tightly coupled to their programming languages like Ruby, Go, Java, Python and PHP, so the language compiler is able to check the correctness of the developer code but does not know how to perform a verification related to the cloud computing field. The developer needs to ignore implementation details and focus on general properties and characteristics. This will help him/her to avoid premature commitment to implementation choices.

Modeling Space

Meanwhile, there is a need for cloud architects to design their applications for multiclouds regardless of the implementation details. For this, model-based solutions are becoming increasingly popular in cloud computing as they provide domain-specific modeling languages and frameworks that enable architects to describe/select/adapt multi-cloud environments. This strategy is summarized as "Model once, generate anywhere". I identify some of the notable model-based solutions for multi-clouds. Unlike programming libraries, they work at a high level of abstraction by focusing on cloud concerns rather than implementation details. I believe that model-driven engineering brings many benefits for multi-clouds [START_REF] Bruneliere | [END_REF]]. Therefore, I focus in the rest of this chapter on detailing the model-driven Cloudware stack and discussing model-based approaches.

Taxonomy of Model-Driven Approaches for the Cloud

In order to understand MDAC and as shown in Figure 2.2, I propose a taxonomy that presents the classification of MDAC literature in terms of three main aspects I identified:

• MDAC usages categorized by the phase of using the approach: design time, deployment time, and production time (Subsection 2.2.1),

• MDAC concepts used to satisfy the corresponding MDAC usages. These concepts may belong to IaaS or PaaS domains, or they reflect transverse cloud concerns like SLA, elasticity, etc. (Subsection 2.2.2), and,

• MDAC characteristics that represent the characteristics of the language used to implement the MDAC, i.e., the paradigm, the syntax and the semantics (Subsection 2.2.3). Chapter 2. Model-Driven Approaches for the Cloud

Model-Driven Approaches for the Cloud

Usages

Usages

Usually, the process of developing an application for/in the cloud is characterized by three main phases: design, deployment and production (i.e., the runtime). For each one, I have identified a set of recurrent usages that can occur during the lifecycle of a cloud application. They are the models which represent, at a high level of abstraction, concrete concerns of cloud management interfaces.

Design Time

This stage regroups the fundamental activities that enact MDAC. It consists for example in migrating a legacy system to the cloud, expressing the client needs by designing and verifying the cloud application requirements, designing the expected cloud environment to focus on cloud concerns rather than the implementation details, selecting the optimum cloud provider that suits the application requirements, refining generic models so they become adapted to represent concrete cloud offerings, exporting cloud models as specifications, documentations, and design artifacts to ease the usage of the cloud systems, etc.

Deployment Time

Once the cloud architecture model is designed, MDAC should be capable to generate the code artifacts in any form for the deployment stage. For example, if the model defined is related to Docker technology [Merkel 2014], MDAC should generate the artifacts corresponding to the model in a form of docker-compose file that can be managed by Docker swarm, or YAML configuration files that can be managed by Kubernetes or OpenShift. In addition, MDAC should be able to generate deployment scripts that can be used by a third-part deployment tools. For example MDAC will be able to generate Ansible playbooks (roles, tasks, host_vars, etc.) [ans], Puppet manifests (resources, classes, modules) [pup], and Chef cookbooks (recipes, templates, etc.) [che].

Production Time

During this phase, MDAC allow the user to have a model representation, i.e., an abstraction of its cloud running system. Then, MDAC will provide a link between the designed architecture and the deployed cloud artifacts on the executing environment. When modifications occur in an existing architecture, MDAC should update the executing environment. Conversely, when changes occur in the executing environment, they should be reflected in the existing architecture. Finally, MDAC will monitor in a real time all the resources deployed in the executing environments and 2.2. Taxonomy of Model-Driven Approaches for the Cloud 29 will report the status in many forms including updating widgets in the designed architecture, or visualizing the monitored facts in a specialized graphs or exporting them as CSV, excel, etc.

Concepts

To implement an MDAC, the designers need to define a set of concepts that represent a specific cloud domain such as infrastructure or platform or related to transverse cloud concerns such as elasticity, Service Level Agreement (SLA) and simulation. Each domain or concern includes a set of specific concepts. For example, VM, container and network integrate the infrastructure domain, whereas server, application and database integrate the platform domain. Each domain-specific concept defines a set of attributes, actions, and constraints. An attribute represents a specific property of this type. An action defines a business specific behavior that can be triggered by a type instance (named also resource). A constraint associated to a type represents a business condition that must be respected by each conforming resource.

Characteristics

MDAC are defined through the use of a metamodel that formalizes the different concepts of the cloud domain. This metamodel defines the modeling language, i.e., the Cloud Modeling Language (CML), which is the bridge between cloud developers and the cloud artifacts. Similar to other languages, a CML is defined in terms of its paradigm, syntax and semantics, which are the three pillars of CML characteristics [Kleppe 2008]. The syntax of a CML may be further divided into an abstract syntax and a concrete syntax.

Paradigm

The paradigm is the manner of thinking when using a language. For example, objectoriented languages involve objects as a paradigm. As for a cloud Domain-Specific

Modeling Language (DSML), its paradigm may rely on the application components, cloud services, cloud resources, or Feature Model (FM)s. On one hand, the paradigm of components is application-oriented since it is used to describe the architecture of the application. The components are thus the entities of an application that the developer needs to deploy on the cloud. On the other hand, services, resources and FMs are cloud-oriented paradigms, i.e., used to describe the cloud offerings. By services, I discuss slightly coupled, shared entities, already deployed in the cloud.

A cloud platform provides services, such as computing and storage, and provides

Abstract syntax

The abstract syntax represents the concepts available in a language and how they are related. For CMLs, the abstract syntax is described by defining a metamodel, which is itself a model that defines the concepts of the domain and how they interrelate. Metamodeling techniques have been standardized by the Object Management Group (OMG) Meta-Object Facility (MOF) [START_REF] Mof | OMG MOF. 2.0 Core Specification[END_REF]] and there are several tools, like the EMF [EMFa], Enterprise Architect [EA], Rational Rose [Rat],

AT OM 3 [Hußmann 2001] etc. that provide metamodeling capabilities. Regarding the abstract syntax, I identify Unified Modeling Language (UML) profiles, Ecore and XML schema.

With UML profiles, we talk about Internal Domain specific language (DSL)s which are limited to the basic language. Although they may draw the libraries and other facilities, they suffer from the lack of abstraction and the paucity of available operations. As for Ecore and XML schema, they are external DSLs, which weakness is the need to create their own tools.

Concrete syntax

The concrete syntax describes a specific representation of the language used to display models to end users. It can be either a textual syntax or a graphical representation, i.e., displayed with a tree-like or a diagram notation. On one hand, the textual syntax is usually defined using a combination of regular expressions and Backus-Naur Form (BNF). On the other hand, the graphical syntax uses a diagram technique with named symbols that represent concepts and lines that connect the symbols and represent relationships. Several tools have been proposed to implement (i) textual concrete syntaxes for DSLs like Xtext [xte 2016] and EMF-Text [emfb], and (ii) graphical concrete syntaxes like Graphical Modeling Framework (GMF) [gmf], Sirius [sir] and Graphiti [gra].

Semantics

The semantics defines well-formedness criteria and gives the meaning of abstract syntax and, indirectly, of concrete syntax. It can be classified into two main categories: static (or structural) semantics and behavioral (or dynamic) semantics. The former defines restrictions on the structure of the designed model, while the latter defines the behavior of the model elements in terms of states, events and interactions. The semantics of CMLs can be explicitly specified using natural language, Object Constraint Language (OCL) constraints and ontologies. However, sometimes the semantic content is not explicitly specified. In this case, domain-specific models are only transformed into artifacts of the implementation or directly executed by a model interpreter that has the potential of facilitating the processing of models at runtime in order to adapt a running application [START_REF] Sousa | [END_REF]], [Fowler 2010]. In this case, the semantics is nothing but the abstraction of the model interpreter.

Model-Driven Approaches for the Cloud

Many MDAC were recently proposed in order to enable abstraction from different implementation languages and platforms. This way, the focus is shifted from the solution space towards the problem space, and from the low-level implementation details towards the higher-level domain specific concepts. The numerous existing MDAC might be overlapping in some aspects and very different in others. Developers require to have means to compare the existing approaches and to select the most appropriate one that fits their needs. Additionally, the lacks of the existing approaches need to be highlighted in order to carry on future work in this field. Consequently, the need for investigating MDAC becomes quite urgent. Across the literature on MDAC surveys, the authors in [START_REF] Bergmayr | [END_REF]] recently presented the most complete state-of-the-art of cloud modeling languages, so far. They surveyed nineteen approaches, that appeared before 2015, in terms of their purposes, characteristics, capabilities and tooling. In my survey, I study twenty-two existing MDAC in terms of the three criteria elaborated in Section 2.2, i.e., usages, concepts and characteristics.

Blueprinting [Nguyen 2012] provides a language that describes cloud services that are combined from a variety of cloud providers, in order to select the best configuration and easily deploy application components in cloud federations while Chapter 2. Model-Driven Approaches for the Cloud crossing SaaS, PaaS and IaaS layers. The current version of Blueprinting is focused on designing blueprints, which are the abstract description of applications assembled in terms of components. As for cloud offerings, they are represented and considered as services, and templates are used to specify the service features. Blueprints are encoded in XML and represented graphically in terms of a Virtual Architecture Topology (VAT). The Blueprinting approach aims to include a detailed and automatized deployment plan that abstracts the technical details of the interaction with a cloud, and reconfiguration actions defined in terms of policies within the WS-Policy or the SLAng languages. To my knowledge, these functionalities are not implemented so far.

Brooklyn [bro] is a framework developed by the Apache consortium for modeling and managing applications through autonomic deployment blueprints textually expressed in YAML in terms of components, and which semantics complies with the CAMP standard. Brooklyn also exposes many of the CAMP REST API endpoints and uses sensors and actuators to provide support for runtime management allowing for dynamically monitoring the application when needed. It introduces vocabulary to describe PaaS capacities and requirements of the application (e.g., databases, containers), and allows the user to define and enforce his/her own reconfiguration policies.

Cloud

Application Modeling and Execution Language (CAMEL) [Kirkham 2014] enables developers to provision IaaS and PaaS, and to deploy application components in multi-clouds. It takes into account several aspects of the application, namely provisioning and deployment topology, provisioning and deployment requirements, service-level objectives, metrics, scalability rules, providers, execution contexts, etc. Therefore, CAMEL considers three types of models: (i) a Configuration Model for selecting the suitable cloud services, (ii) a Deployment Model for hosting the application and (iii) an Execution Model for managing the deployed application. CAMEL exists as an Eclipse plugin, and does not include a graphical interface, but only a textual editor for designing models. CAMEL integrates and extends existing DSLs, such as CloudML [Brandtzaeg 2012[START_REF] Ferry | Towards Model-Driven Provisioning, Deployment, Monitoring, and Adaptation of Multi-Cloud Systems[END_REF], SALOON [START_REF][END_REF]], the Scalability Rules Languages (SRL), and the organization part of CERIF [Asserson 2002]. I believe that CAMEL could be a source of inspiration for the future efforts in modeling the cloud.

Cloud Application Modeling Language (CAML) [START_REF] Bergmayr | [END_REF]] allows cloud architects to represent multi-cloud applications in UML and to select concrete cloud offerings captured by dedicated UML profiles in order to deploy the application components. As an example, Google App Engine (GAE) profile was applied to refine the deployment model of their Petstore reference application, towards concrete cloud offerings provided by the GAE. In this approach, cloud providers that operate at both infrastructure level and platform level are designed. CAML is a UML internal language, presented as a graphical notation, and based on a library, profiles and templates. However, the CAML approach does not include a model interpreter to enact the deployment of multi-cloud applications.

Cloud Adoption Toolkit [Khajeh-Hosseini 2012] is a collection of five tools that provide decision support for the migration of computing services to a cloud environment. It considers a number of factors that may contribute to the impact caused by the migration of an application to the cloud, i.e., cost, energy consumption, stakeholder impact, social and political factors among others. However, their proposal is focused only on the cost model, which includes a number of infrastructure configuration elements, i.e., operating system, server specifications (e.g., CPU clock rate, RAM), storage size, applications, and data already deployed on the VM, among others. The Cost Modeling tool utilizes UML deployment diagrams (i.e., graphical notation), to model an intended architecture for running legacy software in a cloud environment. Later on, price information that enables automated cost estimation for a specific cloud environment is added to the deployment model. These authors work under the assumption that, in most cases, the application deployment is performed on virtual machines. The Cost Modeling tool can model the pricing schemes of multiple cloud providers such as AWS, Microsoft Azure, FlexiScale, etc. However, once the users have created the model, they can select a single cloud provider they wish to use for each of their virtual machines.

Cloud DSL [Silva 2014] is a language that describes infrastructure services from different types of clouds. Then, Cloud DSL maps and adapts entities of the cloud models they propose to platform-specific cloud APIs. Cloud DSL is based on an Ecore metamodel and provides a graphical editor and a textual notation. Cloud DSL has been integrated with TOSCA [START_REF] Binz | [END_REF]]. Using Cloud DSL with TOSCA reduces the workload of creating cloud descriptions in a TOSCA specification.

CloudGenius [START_REF] Menzel | [END_REF]] is a framework mainly used for the selection of appropriate cloud infrastructure services among several ones stored manually and described textually. The Ecore metamodel, on which CloudGenius relies, allows a multi-criteria decision approach from a set of requirements. The latter are based on numerical functional requirements (network latency, technical parameters such as CPU, RAM and storage size, popularity, etc.) and non-numerical functional requirements (operating system, virtual machine format, licence, etc.). Yet, this approach neglects to consider non-functional concerns like the cost, the availability, the response time, etc. A tool prototype named CumulusGenius, used as a Java library, allows the user to programmatically define the requirements that are given as input to CloudGenius selection framework. Then, whenever a solution is found, virtual machines can be executed on top of Amazon EC2 only.

CloudMIG [START_REF] Frey | [END_REF]] is a framework that facilitates the migration of existing software systems to IaaS and PaaS-based cloud environments, which are Amazon EC2 and Google App Engine, respectively. In this approach, cloud environments are modeled as instances of a Cloud Environment Model (CEM) which is an Ecorebased metamodel and for each cloud environment, all possible configurations are modeled. A configuration contains in particular a set of elements and constraints on them. CloudMIG takes as input the legacy software system, and extracts the architectural and utilization models based on the Architecture-Driven Modernization (ADM) principles. From this model, a single compatible cloud environment model candidate is selected. Then, CloudMIG relies on its own constraint validators CloudMIG Xpress [Clo] to check the conformance of the legacy software (the extracted models) with the candidate CEM in terms of constraint violations. The CloudMIG framework is then extended to improve the search of well-suited IaaS environments using search-based genetic optimization.

CloudML [Brandtzaeg 2012[START_REF] Ferry | Towards Model-Driven Provisioning, Deployment, Monitoring, and Adaptation of Multi-Cloud Systems[END_REF], Ferry 2018] is a cloud modeling language that allows both cloud providers and developers to describe cloud services and application components, respectively. Then, it helps to provision cloud resources by a semi-automatic matching between the defined application requirements and the cloud offerings. CloudML is exploited both at design time to describe the application provisioning of cloud resources after performing the necessary orchestration, and at runtime to manage the deployed applications. In fact, the model at design time is automatically handled by the Cloud Modeling Framework (CloudMF), which returns a runtime model of the provisioning resources, according to the Models@run.time approach [START_REF] Blair | [END_REF]. CloudML only provides a JSON and an XML textual syntax to specify deployment and management concerns in IaaS and/or PaaS clouds. CloudML is first introduced in the REMICS project [Sadovykh 2011] as a UML model and developed later by three projects that differ in their objective, i.e., ARTIST [START_REF] Bergmayr | [END_REF]], MODA-Clouds [START_REF] Ardagna | [END_REF]], and PaaSage [paa, Jeffery 2017]. On one hand, REMICS and ARTIST mainly support the migration of legacy software towards a cloudbased environment. In this sense, they adopt UML models since they are reverseengineered and tailored to target cloud systems. In order to extract some semantics, they map the UML models to OpenTOSCA [Binz 2013]. The Cloud target Selection (CTS) [START_REF] Kopaneli | [END_REF]] provides a multi-criteria decision making process for the selection of the cloud target. It combines different types of criteria by using the concepts of CloudML@ARTIST. On the other hand, MODAClouds and PaaSage aim at supporting engineers in building and deploying multi-cloud applications. Therefore, they propose Ecore-based models that include dynamic variability to deal with multiple cloud environments and especially runtime changes. Note that CloudML in PaaSage is the first member of the family of DSLs that form CAMEL.

Farokhi [Farokhi 2014] proposes a framework that assists SaaS providers to select suitable IaaS, which best satisfy their requirements while handling SLA issues. The framework includes three main phases: (1) SLA Construction, (2) Service Selection, and (3) SLA Monitoring and Violation Detection. The Service Selection Engine takes a textual input, an XML file precisely, that describes the SaaS provider requirements. Then, it finds the adequate IaaS providers' services. A breached SLA on runtime will question the selection of the cloud provider and will probably lead to some reconfiguration.

Frey et al. [Frey 2013] focus on selecting near-optimal cloud deployment architectures and defining runtime reconfiguration rules. The main purpose of this approach is to support the migration of software components and their deployment on IaaS environments. To do so, the authors define Cloud Deployment Option (CDO)s which are UML profiles with graphical syntax and constraints written in English prose. Then, they propose CDOXplorer, a genetic algorithm that takes the CDOs as input and analyzes the configuration space of a given cloud provider. Later on, CDOXplorer finds the best configuration based on the average response times and SLA violations. CDOXplorer is implemented in the scope of an open source tool CloudMIG Xpress, that utilizes models which can almost be automatically extracted. The authors in [Frey 2013] assume that the application deployment is always performed on virtual machines. They don't take the principle of containers into account. -Galán et al. [García-Galán 2016] aim to solve the problem of selecting the most suitable configuration among the configuration space offered by a given provider. Their focus is on IaaS. They propose a model that is based on FMs, and apply the automated analysis of FMs as a reasoning technique over the model. Their model can be graphically represented using a tree-like notation, in which features are organized hierarchically. However, their approach did not consider defining a metamodel based on FMs, for the configuration of cloud services. The information to create the FM is automatically extracted from the provider website using an ad-hoc web crawler. This proposal is only applicable to one cloud provider, which is Amazon EC2. However, these authors plan to include different providers in the future. Their model includes cloud configuration elements such as instance type, which determines the configuration of a machine, operating system, storage capability, geographic location, billing information, and customer usage data. Finally, their proposal allows defining constraints on the features and attributes of the model. These constraints are written in English prose. They implemented their proposal and compared their implementation against two commercial tools, Amazon TCO and CloudScreener, and they concluded that their proposal is more expressive and accurate in terms of providing a wider range of configuration options and choosing the most suitable configuration.

Garcia

Gherardi et al. [START_REF] Gherardi | [END_REF]] claim to present the first paper that combines robotics, cloud computing, and SPLs. It is interested in configuring and deploying complex Robot as a Service (RaaS) only on top of Rapyuta [Mohanarajah 2015], an open source robotic PaaS. Decisions regarding what components of Rapyuta to employ and how to compose them (the connections) are taken by exploiting three models via a Resolution Engine. The first two models are a reference architecture which is an Ecore metamodel reflecting the requirements of the application, and an extended FM, i.e., a FM that enriches the features in a model with attributes in order to improve the semantics. The third model is the glue between the first two models and specifies how the variability can be resolved. Feature Selector tool for creating a selection of features reflecting the requirements of their application. Graphical editors are used to design the models, that are described within a textual syntax too.

Holmes [Holmes 2014] proposes three textual languages based on an Ecore metamodel for expressing and capturing IaaS concepts, then provisioning a customized stack of cloud services, via model transformations. From the DSL programs and the supplied Puppet [pup] modules, the entire cloud service stack is automat-ically built, without further user interaction. Later on, in order to reconfigure the deployment and achieve the new requirements of the system, reverse-engineering is used to capture the differences between models. Therefore, for dealing with differential changes of IaaS models, Holmes [Holmes 2015] proposes a model-based roundtrip engineering approach that combines the power of model-driven generation with runtime reflection, i.e., this approach does not only incorporate models from design time but also Models@run.time. This approach allows to compare and migrate infrastructure services between two clouds. They consider a migration from Open-Stack 2012.1 to OpenStack 2013.2. For orchestration, they employ Nova API [nov], which is OpenStack native.

MOve to Clouds for Composite Applications (MOCCA) [START_REF] Leymann | [END_REF]] is a method for moving legacy applications to the cloud. It introduces an Ecore metamodel for specifying the applications that are modeled in terms of components. The model semantics is described with natural language and can also be deduced by the behavior of the deployment optimizer in use. The authors also propose Cafe [START_REF] Mietzner | [END_REF]], a prototypical tool supporting the MOCCA method and offering graphical and textual modeling of the application architecture and topology. The MOCCA method allows for provisioning infrastructure resources that are described in OVF files which perform the required adaptation for the components deployment. Cafe assumes that an OVF file represents only one component. In case an OVF file contains the virtual image of more than one component (i.e., more than one virtual system), this file must be split into separate OVF files manually. Thus, Cafe does not support the notion of multiple clouds. However, the authors of this method state that a future extension of Cafe will support OVF files with virtual images of multiple components.

MULTICLAPP [START_REF] Guillén | [END_REF]] is a framework for modeling components of multi-cloud applications which are not dependent of any specific cloud provider. This framework is based on a UML profile, with a graphical editor to model components that are expected to be deployed on PaaS cloud environments by applying cloud provider independent stereotypes to them. These stereotypes enable the application developers to select the cloud provider offerings that are best for deploying the application components. Applications that are fully modeled are processed by a deployment engine, which generates each of the cloud artifacts identified in the deployment plan. Each artifact is adapted in order to comply with the specifications of its assigned platform. Once they are generated, the artifacts can be deployed in their cloud platforms.

Chapter 2. Model-Driven Approaches for the Cloud

OpenTOSCA [opeb] is an ecosystem developed by the University of Stuttgart that aims to provide modeling tool support and runtime support for the TOSCA standard [START_REF] Binz | [END_REF]]. Several implementations of OpenTOSCA were developed. For example, (i) Winery [Kopp 2013] provides an open source Eclipse-based graphical modeling tool for TOSCA topologies/structures/architectures, i.e., the software components that constitute the application, the physical or virtual nodes on which the components will be deployed, and the relationships between components and nodes, and (ii) OpenTOSCA runtime [Binz 2013] provides an open source container for deploying TOSCA-based applications defined in a Cloud Service ARchive (CSAR) packaging format. The OpenTOSCA runtime is hence responsible for translating a TOSCA topology into actions to be performed in clouds. These actions are sent to the clouds through their respective APIs. Despite TOSCA language manages to cover the infrastructure and platform service stack, it is only defined as a textual XML document or YAML document so it is complicated to have an overview of the supported cloud entities. Furthermore, TOSCA does not employ the typical cloud vocabulary, such as services and resources. Instead, it defines a set of abstract elements, such as nodes and relationships to respectively designate cloud services and how they interact. Therefore, designing a TOSCA topology requires the effort of a human developer, which is a time consuming and an error-prone activity. The application deployment to the target cloud and its management are provided by orchestration plans written within different workflow languages,e.g., BPMN or BPEL. However, in case some module of the application is migrated to a different target provider, the topology and the orchestration plan should be modified which makes the management of a TOSCA-compliant deployment a complex task. [START_REF] Chapman | [END_REF]] offers a language for the description of requirements that providers must fulfill when the developers deploy a multi-component application on federated IaaS clouds. Among these requirements, it takes into account non-functional requirements such as quality of service. The RESERVOIR-ML language encodes the OVF standard within XML and its semantics is described within OCL constraints. Beside describing the requirements, the main focus of this approach is also to perform reconfiguration tasks and address the scaling requirements of the application components, i.e., to ensure elasticity and provision IaaS resources on demand. To do so, the RESERVOIR-ML project has also developed UCL-MDA tools, a graphical framework implemented as a plugin for the Eclipse Integrated Development Environment (IDE) for the manipulation of the XML models and the OCL constraints.

RESERVOIR-ML

SALOON [START_REF][END_REF]] is a graphical framework for cloud environments selection and configuration purpose. SALOON is an EMF-based framework that relies on extended FMs to represent clouds variability, as well as on ontology concepts to model the various semantics of cloud systems. It mainly comprises functional elements such as the language used to develop the cloud-based application, the number of application servers, the RAM, the CPU, etc. This proposal also allows to translate the ontology concepts into a Constraint Satisfaction Problem (CSP) in order to select the adequate cloud environment. In order to extract the information to create the models for each cloud provider, the authors suggest the use of reverse engineering on the web configurator of each cloud provider as a solution. They implemented their proposal and tested the performance of their implementation. They concluded that their proposal was well suited to handle large configuration spaces, with a number of features and constraints that would make it overwhelming for a human user to perform the selection by hand. Despite that the authors state that SALOON supports the discovery and selection multiple providers, in practice it does not. In the contrary, it deals with one provider at a time. SALOON targets ten cloud environments (IaaS and PaaS).

soCloud [START_REF] Paraiso | soCloud: A Service-Oriented Component-based PaaS for Managing Portability, Provisioning, Elasticity, and High Availability across Multiple Clouds[END_REF]] is an approach that aims at developing multi-cloud applications by defining a PaaS platform based on FraSCAti, a Service Component Architecture platform. soCloud defines its concepts within an XML schema. It provides a textual syntax and its semantics is written in English Prose in the context of the SCA specification that is implemented in FraSCAti. soCloud targets fifteen cloud environments (IaaS and PaaS), where it allows deploying and reconfiguring application components after achieving the necessary orchestration.

Sousa et al. [START_REF] Sousa | [END_REF]] aim to generate reconfiguration plans that satisfy the requirements of a multi-cloud computing system. To do so, the authors propose an Ecore metamodel to model FMs and capture the variability of cloud configurations. The multi-cloud constraints that arise during the cloud reconfiguration are defined by Linear Temporal Logic (LTL) formulas to express temporal properties. The authors applied their approach only to Heroku cloud PaaS and they manually built their FM by going through the Heroku documentation.

StratusML [START_REF] Hamdaqa | [END_REF]] is a layered modeling language and a modeling framework for cloud applications. StratusML provides a user-friendly interface that allows the cloud developers to specify their application components, configure them, estimate cost under diverse cloud services, select a cloud provider, use templates to transform and adapt the model into platform specific artifacts, and manage the application behaviour at runtime through a set of rules. It is built as an extension of Microsoft Visual Studio 2012, i.e., the Microsoft DSL toolkit is used to design the StratusML graphical editor and to define the validation constraints. The latter are required to ensure that the specified model satisfies the application requirements and provides the information required to generate the target platform specific artifacts. The validation constraints can be classified into hard constraints, i.e., that the user can never violate, and soft constraints, i.e., that are allowed to be violated, but still create warnings and errors to guide the user to the correct decisions. In order to capture the application deployment configuration, the StratusML metamodel integrates five different models to address five different, but interleaved functional and non-functional cloud concerns. It includes the service model, performance model, adaptation model, availability model, and provider model. StratusML uses layers to view the different cloud application concerns, facilitating visual modeling of adaptation rules, and using template-based transformation to deal with platforms heterogeneity. StratusML has established a connector only with the Windows Azure IaaS.

Discussion

Conclusion 1. Primary focus on design time aspects

As depicted in Table 2.2, most of the MDAC only provide the possibility to set the resources (CPU, memory, disk, network, etc.) limits at design time. However, they lack of resources management at runtime. The management is necessary because in the cloud environment, the resources consumption fluctuates according to the workload. In order to provision the appropriate resources, if the workload grows or shrinks, the resources should be reconfigured, i.e., increased or decreased as required at runtime. Thus, a major challenge is how to synchronize the predefined architecture of resources with the resources provisioned in the execution environment. When modifications occur in an existing architecture, the update should be done in the executing environment. Conversely, when changes like the increase of the disk storage or the addition of a virtual machine occur in the executing environment, they should affect the existing architecture. It is thus required that an MDAC reduces the gap between design and runtime activities and provides the same model for both of them.

We tackle this problem in Chapter 3 by providing a complete tool chain to handle cloud resources during their whole lifecycle, from the design till the management.

Conclusion 2. Primary focus on IaaS

As depicted in Table 2.3, the largest amount of researchers attention has been focused on IaaS clouds. An efficient MDAC should allow to handle infrastructure, platform and software resources. There is a strong separation between these three types of resources since each of them is managed by a particular resource manager. These managers do not know how to cooperate. Thus it is extremely difficult to implement policies for the management of multi-level resources. However, in order to manage the elasticity of a system for example, the cloud developer needs to manage simultaneously resources at IaaS, PaaS and SaaS levels. Therefore, there is a need for a single MDAC that includes concepts and mechanisms that support both IaaS and PaaS clouds, enabling their management.

We also tackle this problem in Chapter 3. In fact, our proposed tool chain for the cloud computing complies to OCCI, the only generic and extensible standard that handles every kind of cloud resources, i.e., IaaS, PaaS, SaaS and even RaaS and Container as a Service (CaaS).

Conclusion 3. Fuzziness of the CML concepts

Most of the MDAC are built from scratch; the designer of the CML goes through the provider or the application documentation, and then manually defines the concepts that he/she considers important to be included to the provider or the application metamodel. This methodology results in the fuzziness of the CML which might be unrepresentative of the concrete cloud environment. Also, the MDAC I reviewed in this chapter describe a part of the cloud domain that was relevant only at the moment of the definition of the modeling language. However, the designers of each MDAC require changing their modeling language, i.e., the CML, at each time they want to support more cloud concepts. As for the user, he/she is unable to add the missing concepts that he/she needs.

I tackle this problem in Chapter 4 where I propose the first advanced approach for automatically inferring a cloud model that properly represents the cloud concepts and operations. This model can be updated to follow up with the cloud API and since it conforms to the generic OCCIware Metamodel, this model can be extended to support new concepts. It also helps analyzing the cloud API and enhances its specification so the developer can correctly use its services.

Conclusion 4. Little attention paid to the semantics

We observe in Table 2.4 that the semantics of the CMLs is, in most cases, either informal, namely written in English prose or within OCL constraints, or implicit in the model interpreter behaviour. None of these ways of defining the semantics is sufficiently precise. Natural language might be confusing due to its built-in ambiguity; although words with multiple meanings give English a linguistic richness, they also create ambiguity. OCL is semi-formal, i.e., its syntax is well-defined but its semantics is only partially formalized, with many aspects being just described in natural language in the standard document specifications. Also, OCL is efficient for only specifying the static semantics of the CMLs. Dynamic semantics remains defined within natural language. Finally, the model interpreter is the engine that is fed the deployment, configuration, adaptation models in order to execute them. Deriving the semantics of these models from the behaviour of the model interpreter might be erroneous. It is crucial then to propose CMLs with well-formed semantics, i.e., defined within formal methods which are mathematical techniques that allow the cloud stakeholders to reason and describe without ambiguity the structure metamodel and the behavior of its concepts.

I tackle this problem in Chapter 5 where I propose the first formal framework for precisely specifying cloud APIs and reasoning over them. Consequently, the developer can verify the correctness of his/her cloud models and their required behaviour.

Summary

The wide number of available cloud providers, their high heterogeneity and semantic differences make it complicated to exploit multi-cloud assets. In this chapter, I provided a classification of Cloudware engineering solutions. I showed that the solutions at the provider and the programming spaces are also heterogeneous and their provided features are often incompatible. This diversity hinders the proper exploitation of the full potential of cloud computing, since it prevents interoperability and promotes vendor lock-in, as well as it increases the complexity of development and administration of multi-cloud systems.

To deal with this heterogeneity, I introduced the solutions at the modeling space and explained the major role that models play in the software development for the cloud computing. I discussed the idea of "Modeling the cloud computing" by leveraging MDE to easily build cloud-native applications. I discussed the usages, concepts and characteristics of MDAC. Finally, I reviewed the most relevant approaches in the research area that is closely related to this thesis, i.e., model-driven engineering for cloud computing. Among the prolific research in this area, there is a lack of solutions which:

Summary

• support design, deployment and management usages,

• allow handling XaaS systems,

• define the appropriate cloud concepts with possibility of extension if needed, and,

• define a precise semantics of these concepts.

Based on this study, I describe in the next parts of this dissertation the OC-CIware background and the two contributions of this thesis respectively. I mainly propose to leverage MDE and formal methods to help cloud stakeholders taking better advantage of cloud services.

Part III

Background

In the end of Part II, I discussed the need of precisely describing but also efficiently managing every kind of cloud resources. To accomplish this purpose, I detail in this part our OCCIware approach.

Chapter 3

Modeling, Verifying, Generating and Managing Cloud Resources with OCCIware

This chapter corresponds to our article "Model-Driven Cloud Resource Management with OCCIware" [Zalila 2018] submitted to the Future Generation Computer Systems (FGCS) journal, which extends our paper "A Model-Driven Tool Chain for OCCI" [Zalila 2017a] published in the 25th International Conference on Cooperative Information Systems (CoopIS). S everal cloud computing standards have been proposed to resolve the hetero- geneity of cloud providers and promote multi-clouds, as discussed in Chapter 2.

Chapter 3. Modeling, Verifying, Generating and Managing Cloud Resources with OCCIware However, the main drawback of these standards is their specificity for a particular cloud service model, i.e., IaaS or PaaS.

OCCI has been proposed as the first and only open standard for managing any cloud resources [START_REF] Edmonds | Toward an Open Cloud Standard[END_REF]]. OCCI provides a general purpose model for cloud computing resources and a RESTful API for efficiently accessing and managing any kind of these cloud resources. This will ease interoperability between clouds, as providers will be specified by the same resource-oriented model called the OCCI Core Model [Nyrén 2016b], that can be expanded through extensions and accessed by a common REST [Fielding 2000] API.

Currently, only runtime frameworks such as rOCCI [roc], erocci [ero], pySSF [pys], pyOCNI [pyo], and OCCI4Java [occb] are available, while OCCI designers/developers/users need software engineering tools to design, edit, validate, generate, implement, deploy, execute, manage, and supervise new kinds of OCCI resources, and the configurations of these resources. In addition, the existing runtime implementations are targeting a specific cloud service model (mainly IaaS). Thus, OCCI lacks a unified modeling framework to design its different artifacts, and verify them during the initial steps of the design process before their effective deployment. Added to that, OCCI stakeholders need a generic runtime implementation coupled with the expected modeling framework in order to seamlessly execute the different developed and/or generated artifacts. Finally, as OCCI is proposed as an open generic standard to manage XaaS, OCCI stakeholders need to obtain, for each domain, a specific modeling framework.

To overcome the issues presented above, I present in this chapter our OCCIware approach, which can be summarized as:

• Model-Driven Managing Everything as a Service with OCCIware.

OCCIware is a model-driven vision to manage XaaS. It allows one to model any type of resources. It provides OCCI users with facilities for designing, editing, validating, generating, implementing, deploying, executing, managing, and supervising XaaS with OCCI.

• Generating Cloud Domain-Specific Modeling Frameworks with OC-CIware. OCCIware is a factory of cloud domain-specific modeling frameworks. Each generated Cloud Domain-Specific Modeling Studio (CDSMS) is dedicated for a particular cloud domain. Each CDSMS can be used to design configurations conforms to its related domain and hides the generic concepts of OCCI. This work has been done in the context of the OCCIware research and devel-3.1. Motivations 51 opment project1 funded by the French PIA. The contribution of the academic and industrial partners has certainly promoted the progress of this project. A special gratitude is due to Faiez Zalila and Christophe Gourdin who implemented the OCCIware approach.

This chapter is structured as follows. Section 3.1 explains the motivations behind

OCCIware. Section 3.2 gives a background on the OCCI standard. Section 3.3 presents an overview of the OCCIware approach. It details the different processes to use the OCCIware approach. Section 3.4 presents the OCCIware Metamodel by detailing its static semantics defined in Ecore and OCL. Section 3.5 provides an overview of OCCIware Studio and its different implemented features. Section 3.6 presents OCCIware Runtime and details its architecture. Section 3.7 validates

OCCIware by presenting the different OCCI extensions defined by the standard and implemented using OCCIware. We follow up with the evaluation of OC-CIware by discussing different five use cases implemented with the OCCIware approach. Finally, Section 3.8 concludes with future work and perspectives.

Motivations

Currently, cloud architects and developers have a lot of hope for the multi-cloud computing paradigm as an alternative to avoid the vendor lock-in syndrome, to improve resiliency during outages, to provide geo-presence, to boost performance and to lower costs. However, semantic differences between cloud provider offerings, as well as their heterogeneous CRM-APIs make migrating from a particular provider to another a very complex and costly process. We assume for example that a cloud developer would like to build a multi-cloud system spread over two clouds, AWS and GCP. AWS are accessible via a SOAP-based API, whereas GCP is based on a REST API, which leads to an incompatibility between these two different APIs.

To use them, cloud consumers should be inline with the concepts and operations of each API, which is quite frustrating. The cloud developer would like a single API for both clouds to seamlessly access their resources.

For this, OCCI is an open standard that defines a generic extensible model for any cloud resources and a RESTful API for efficiently accessing and managing cloud resources. This will facilitate interoperability between clouds, as cloud provider's offerings will be specified by the same resource model, and accessed by a common REST API. However, cloud developers cannot currently take advantage of this standard. Although there are several implementations of OCCI, there is no tool that allows them to design and verify their configurations, neither to generate and deploy Resources with OCCIware corresponding artifacts. This leads to several challenges: 1. Cloud architects, who are supposed to design the expected multi-cloud platform, are facing on one side to heterogeneity at different levels such as CRM-APIs heterogeneity (REST APIs vs SOAP APIs), service models heterogeneity (IaaS, PaaS, SaaS, etc.), deployment model heterogeneity (public, private and hybrid), and service providers heterogeneity. On the other side, cloud developers, who create and deploy running cloud systems, are focused on implementation details rather than cloud concerns, with the risk of misunderstandings for the concepts and the behavior that rely under cloud APIs. They need a customized cloud framework dedicated to each cloud domain.

2. The only way to be sure that the designed configurations will run correctly is to deploy them in the clouds. In this context, when errors occur, a correction is made and the deployment task can be repeated several times before it becomes operational. This is quite painful and expensive.

3. Cloud developers need to provide various forms of documentation of their cloud configurations, as well as deployment artifacts. However, these tasks are complex and usually made in an ad-hoc manner with the effort of a human developer, which is error-prone and amplifies both development and time costs.

4. The CRM-APIs heterogeneity represents a banner to seamlessly execute the deployment artifacts.

5. At the design level, the configuration represents a predefined architecture. However, the execution environment hosts a deployed system. A main challenge to the cloud developers is to provide a synchronization between the design level and the execution environment. When modifications occur in the predefined architecture, the update should be done in the executing environment. Conversely, when the deployed system changes, it should affect the predefined architecture.

Recently, we are witnessing several works that take advantage of MDE for the cloud [START_REF] Bruneliere | [END_REF][START_REF] Bergmayr | [END_REF]]. Therefore, to address the identified challenges, we believe that there is a need for a tooled model-driven approach for OCCI in order to:

1. Enable both cloud architects and developers to efficiently design their needs at a high-level of abstraction. This will be done by defining a metamodel, as a DSML, accompanied with graphical and textual concrete syntaxes. The expected DSML should be extensible in order to target different cloud domains.

Background on OCCI 53

2. Allow cloud architects to define structural and behavioral properties and verify them before any concrete deployments so they can a priori check the correctness of their cloud systems.

3. Automatically generate and export (i) textual documentations to assist cloud architects and developers to understand the concepts and the behavior of cloud-oriented APIs, (ii) specific designers dedicated to each cloud domain to assist cloud developers in the design of their configurations, (iii) formal specifications in order to formally analyze the different artifacts, and (iv) HTTP scripts that deploy, provision, modify or de-provision cloud resources.

4. Execute the generated scripts into a generic OCCI runtime implementation that must be able to host the developed connectors to concrete cloud resources.

5. Discover a configuration model by mapping a running cloud system into the expected modeling framework, manage this running cloud system via the configuration model (for example, execute an action on the configuration model implies its execution on the running cloud system), and bring back the updates of the running system into the corresponding configuration model. These processes can be ensured via a connector between the cloud system and the modeling framework.

Background on OCCI

OCCI is an open cloud standard [START_REF] Edmonds | Toward an Open Cloud Standard[END_REF]] specified by the OGF. OCCI defines a RESTful Protocol and API for all kinds of management tasks on any kind of cloud resources, including IaaS, PaaS and SaaS. In order to be modular and extensible, OCCI is delivered as a set of specification documents divided into the four following categories as illustrated in Figure 3.1: Resources with OCCIware Resource represents any cloud computing resource, e.g., a virtual machine, a network, an application container, an application. Link is a relation between two

OCCIware Approach 55

Resource instances, e.g., a computer connected to a network, an application hosted by a container. Entity is the abstract base class of all resources and links. Kind is the notion of class/type within OCCI, e.g., Compute, Network, Container, Application. Mixin is used to associate additional cross-cutting features, e.g., location, price, user preference, ranking, to resource/link instances. Action represents an action that can be executed on entities, e.g., start a virtual machine, stop an application container, restart an application, resize a storage. Category is the abstract base class inherited by Kind, Mixin, and Action. Attribute represents the definition of a customer visible property, e.g., the hostname of a machine, the IP address of a network, or a parameter of an action. OCCI Protocols. Each OCCI Protocol specification describes how a particular network protocol can be used to interact with the OCCI Core Model. Multiple protocols can interact with the same instance of the OCCI Core Model. Currently, only the OCCI HTTP Protocol [Nyrén 2016a] has been defined. But other OCCI protocols would be proposed in the future such as Advanced Message Queuing Protocol (AMQP).

OCCI Renderings. Each OCCI Rendering specification describes a particular rendering of the OCCI Core Model. Multiple renderings can interact with the same instance of the OCCI Core Model and will automatically support any OCCI extension. Currently, both OCCI Text [Edmonds 2016] and JSON 2 [Nyrén 2016d] renderings have been defined. Other OCCI renderings would be specified in the future, such as an XML rendering for instance. OCCI Extensions. Each OCCI Extension specification describes a particular extension of the OCCI Core Model for a specific application domain, and thus defines a set of domain-specific kinds and mixins. OCCI Infrastructure [Nyrén 2016c] is dedicated to IaaS. Additional OCCI extensions are defined such as OCCI Compute Resource Templates Profile (CRTP) [START_REF] Drescher | [END_REF]], OCCI Platform [START_REF] Metsch | [END_REF]] and OCCI SLA [Katsaros 2016].

OCCIware Approach

Managing Everything as a Service with OCCIware

The OCCIware funded project [occc, Parpaillon 2015] aims to provide a formal comprehensive, coherent, modular, model-driven tool chain for managing any kind 56 Chapter 3. Modeling, Verifying, Generating and Managing Cloud Resources with OCCIware of cloud computing resources. The OCCIware approach relies on MDE, a software engineering paradigm that proposes to reason on high-level artifacts, called models, rather than the code implementation. As MDE allows us to raise the level of abstraction, a model is an abstract representation of a system. It allows us to understand the designed system and answer the related queries. A model conforms to a metamodel, which defines the modeling language.

The OCCIware approach is composed of two main components as depicted in Figure 3. OCCIware Studio, detailed in Section 3.5 is an OCCI model-driven tool chain that enables to design, verify, simulate, and develop every kind of resources as a service. Usually, a model-driven approach is based on, at least, a metamodel. The OCCIware approach is designed and developed based on a metamodel, called OCCIware Metamodel and detailed in Section 3.4. This metamodel implements and extends the OCCI Core Model.

OCCIware Runtime detailed in Section 3.6 is a generic OCCI-compliant Models@run.time support and includes a resources container, and tools for deployment, execution, and supervision of XaaS.

To benefit from the OCCIware approach, a proposed process must be followed (cf. Figure 3.4). This process has three steps: the design step, the engineering step, and the use step.

Design step

The design step (the top of Figure 3.4) consists in defining a new OCCI extension that extends the OCCI Core extension (an extension-like representation of the OCCI Core Model), and/or other OCCI extensions already defined. This step is ensured by the Cloud Architect who aims to have a tooled model-driven framework for his/her cloud domain such as infrastructure, platform, etc. An OCCI extension model conforms to OCCIware Metamodel. It can be designed textually and/or graphically. Once the extension is designed and validated, a generation process of the Extension Tooling may be triggered. It consists to generate, from an OCCI extension model, a set of artifacts that meet the needs of the cloud developers.

The set of artifacts generated from an OCCI extension model can be summarized as:

1. Extension Documentation represents a comprehensive documentation of the designed extension. It serves as the reference document to describe for the cloud developer the different notions designed in the extension.

2. Extension Formal Specification defines formally the specification of the designed extension. This artifact can be later analyzed using a dedicated tool to check rigorously its correctness and its conformance to the OCCI specifications. This extension is detailed in Chapter 5.

3. Extension Metamodel is a modeling language dedicated to the domain of the designed extension. It allows us to design conforming models representing running systems of this domain. This metamodel extends the OCCIware Metamodel.

Extension Implementation

Engineering step

Once the previous step is achieved, the Software Developer can complete the generated Extension Connector. It consists of implementing the business code required to handle each concept of the extension. Later, the completed connector must be deployed on OCCIware Runtime. Finally, he/she customizes the generated Extension Designer to adapt it to the dedicated domain and to abstract the different concepts of the extension. From now on, we can consider that the Extension Tooling is able to be used to manage conforming configurations.

Use step

Thanks to OCCIware Studio enriched with the Extension Tooling provided during the previous steps, the cloud developer, who is the System Engineer (end user from our perspective), can design using the dedicated Extension Designer, an Extension configuration model conforms to the Extension Metamodel. For the system engineer, the different OCCIware tooling is entirely hidden because he/she only deals with domain concepts such as VMs, containers, networks, etc.

To benefit from the OCCI-compliant tools of OCCIware (i.e., OCCIware Runtime), the Extension configuration model must be translated into an OCCI configuration model that conforms to the OCCIware Metamodel. Both models are semantically identical, but the first one instantiates the concepts of the generated Extension Metamodel, and the second instantiates the concepts of OCCIware Metamodel.

In order to deploy and manage this generated configuration, the cloud developer can interact with the cloud by sending OCCI HTTP requests to OCCIware Runtime extended with the deployed Extension Connector. These scripts can be generated from the OCCI configuration model. To execute them, OCCIware Runtime invokes the appropriate Extension Connector to create the instance in the cloud. Finally, the created resource is deployed in the cloud.

Generating Cloud Domain-Specific Modeling Studios with

OCCIware

As previously explained in Subsection 3.3.1, the OCCIware approach provides a set of tools to design, edit, validate, generate, and manage OCCI artifacts. Concretely, the main goal of OCCIware Studio consists in designing, at the end, a correct OCCI configuration model that conforms to the OCCIware Metamodel. Moreover, the ultimate goal for the cloud developer, the end user of the OCCIware approach, consists in executing this model that represents an eventual running system in the cloud. In the OCCIware approach, executing a configuration model invokes the OCCIware Runtime to create the different designed entities. During modeldriven development, two strategies to execute models are possible [START_REF] Brambilla | [END_REF]]:

Code Generation and Model Interpretation.

Code Generation targets to produce running artifacts (script, code, etc.) from a higher level model. It is similar to the compilation that produces executable binary files from source code. Usually, the generated artifact is produced in a standard language that any developer can understand. In addition, the code generation strategy allows us to link a model-driven framework to existing tools and methods such as model-checkers, simulators and runtime environments.

Model Interpretation approach consists of parsing and executing the model on the fly, with an interpretation approach and using a generic engine. A major advantage of this approach is the capability to change the model at runtime without stopping the running application because the interpreter would continue the execution by parsing the new version of the model.

In the OCCIware approach, as shown on the left part of Figure 3.5, both strategies have been implemented. Code generation process allows us to integrate a generator of HTTP requests from OCCI configuration models. These requests can be later sent to OCCIware Runtime to create and deploy OCCI entities. The extensibility of OCCIware Studio lets software engineers implement additional generators to target other existing tools for other purposes such as the generation of deployment plans. Model interpretation is implemented by defining a Runtime Connector. Using this connector, we can (i) discover a configuration model by mapping a running system from OCCIware Runtime to OCCIware Studio, (ii) edit the obtained configuration model, (iii) send these modifications to the running system, and finally (iv) bring back the changes triggered by the runtime to the model.

OCCIware Studio represents the first model-driven framework to design OCCI artifacts. In addition, thanks to the different proposed generators, OCCIware Studio can be considered as a factory to build cloud domain-specific modeling studios, each one is specific to a particular cloud domain. As shown on the right part of Figure 3.5, once an OCCI extension model is defined, we can proceed to the generation of a Cloud Domain-Specific Modeling Studio (CDSMS) dedicated to a particular cloud domain. This specific studio provides (i) an Extension Metamodel, (ii) an Extension Validator, (iii) an Extension Implementation, and (iv) an Extension Designer. These generated tools allow the cloud developer to design configurations conform to a specific cloud domain. As OCCIware Studio, a specific studio can support both strategies to execute the designed Extension config-

OCCIware Metamodel

Designing is the key activity that must, at first, be addressed to later resolve other encountered challenges such as verifying, generating, and deploying. Therefore, in order to assist OCCI users in modeling different OCCI artifacts, a metamodel for OCCI named OCCIware Metamodel3 is proposed, as shown in Figure 3

OCCIware Metamodel 63

The entry point to define OCCIware Metamodel was the OCCI Core Model [Nyrén 2016b]. The gray-colored classes in Figure 3.6 show the eight concepts of OCCI Core Model. The blue-colored classes show the added concepts during our previous work [Merle 2015a]. Since then, we continued to extend OCCIware Metamodel in order to meet different needs appeared during its use. The browncolored classes introduce the added concepts needed to express business constraints related to a particular domain. The orange-colored class represents the required concept to instantiate the mixins in a configuration model. The yellow-colored classes define the concepts used to express the behavior of an OCCI kind/mixin. The cyan-colored classes provide the required concepts to express non-OCCI core information needed to perform several activities such as code generation and model visualization. The green-colored classes define the OCCIware data type system. Finally, the red-colored classes provides a set of Ecore data types required to create correct OCCI artifacts.

In the following, the different concepts of the OCCIware Metamodel with a subset of their associated OCL invariants defining the static semantics are detailed:

• Extension represents an OCCI extension, e.g., inter-cloud networking extension [START_REF] Medhioub | [END_REF]], infrastructure extension [Nyrén 2016c], platform extension [START_REF] Yangui | [END_REF], Yangui 2016[START_REF] Metsch | [END_REF], application extension [Yangui 2016], SLA negotiation and enforcement [Katsaros 2016], cloud monitoring extension [START_REF] Ciuffoletti | Open Cloud Computing Interface -Monitoring Extension[END_REF]], and autonomic computing extension [START_REF][END_REF], Mohamed 2014b, Mohamed 2014a[START_REF][END_REF]].

Extension has a name, has a scheme, has a description, has a specification, owns zero or more kinds, owns zero or more mixins, owns zero or more data types, and can import zero or more extensions. Each designed extension must, at least, extend the OCCI Core extension, the extension-like representation of the OCCI Core Model. The OCCI Core extension is composed of three kinds: a root Entity kind, and two children kinds, Resource and Link.

Definition 1 Each Extension instance must have a unique scheme among all Extension instances.

c o n t e x t E x t e n s i o n i n v a r i a n t UniqueScheme : E x t e n s i o n . a l l I n s t a n c e s ( )->i s U n i q u e ( scheme ) ;

Definition 2

The scheme of all kinds must be equal to the scheme of the owning Extension instance.

Chapter 3. Modeling, Verifying, Generating and Managing Cloud Resources with OCCIware c o n t e x t E x t e n s i o n i n v a r i a n t KindsSchemeValid : k i n d s ->f o r A l l ( k | k . scheme = s e l f . scheme ) ;

• Kind is an OCCI Core Model concept representing the immutable type of OCCI entities and defines allowed attributes and actions. Single inheritance, using the parent relation between Kinds, allows us to factorize attributes and actions common to several kinds. The source and target references specify the sense of relations between link-oriented kinds.

Definition 3 Each Kind instance must inherit from the entity kind instance directly or transitively. The entity kind instance is the root of the hierarchy of Kind instances.

c o n t e x t Kind i n v a r i a n t E n t i t y K i n d I s R o o t P a r e n t : s e l f ->c l o s u r e ( p a r e n t )->e x i s t s ( k | k . term = ' e n t i t y ' and k . scheme = ' h t t p : // schemas . o g f . o r g / o c c i / c o r e# ' and k . p a r e n t = n u l l ) ; Definition 4 A Kind instance must not overload an inherited attribute.

c o n t e x t Kind i n v a r i a n t A t t r i b u t e s N a m e N o t A l r e a d y D e f i n e d I n P a r e n t : a t t r i b u t e s . name->e x c l u d e s A l l ( parent ->c l o s u r e ( p a r e n t ) . a t t r i b u t e s . name ) ;

• Mixin is an OCCI Core Model concept representing cross-cutting attributes and actions that can be dynamically added to an OCCI entity. Mixin can be applied to zero or more kinds and can depend on zero or more other Mixin instances.

Definition 5 The inheritance relation depends between Mixin instances must form a direct acyclic graph. A mixin instance must not inherit from itself directly or transitively. • Type is an added concept to represent an abstract type inherited by Kind and Mixin classes. Each type can own zero or more actions, zero or more constraints and a Finite State Machine (FSM) describing its behavior.

Definition 6 Each action instance must have a unique scheme among all action instances in a Type instance.

c o n t e x t Type i n v a r i a n t ActionTermUnicity : a c t i o n s ->i s U n i q u e ( term ) ;

Definition 7 Each constraint instance must have a unique name among all constraints instances in a Type instance.

c o n t e x t Type i n v a r i a n t ConstraintNameUnique : c o n s t r a i n t s ->i s U n i q u e ( name ) ;

• Action is an OCCI Core Model concept representing business specific behaviors, such as start/stop a virtual machine, and up/down a network, etc.

• Constraint is an added concept to represent a detailed aspect related to a particular cloud computing domain. In fact, each extension targets a concrete cloud computing domain, e.g., IaaS, PaaS, SaaS, pricing, etc. Therefore, there are certainly business constraints related to each domain, which must be respected by configurations that use the extension. For example, all IP addresses of all network resources must be distinct. A Constraint has a name, a description and a body that can be defined with Object Constraint Language (OCL) [START_REF] Omg | OMG. Object Constraint Language[END_REF]].

• Category is an OCCI Core Model concept and the abstract base class inherited by Type and Action. Each instance of kind, mixin or action is uniquely identified by both a scheme and a term, has a human-readable title, a description, and owns a set of attributes.

Definition 8 The scheme of each Category instance must end with a sharp.

c o n t e x t Category i n v a r i a n t SchemeEndsWithSharp : scheme . s u b s t r i n g ( scheme . s i z e ( ) , scheme . s i z e ( ) ) = '# ' ;

• Attribute is an OCCI Core Model concept and represents the definition of a customer-visible property, e.g., the hostname of a machine, the IP address of a network, or a parameter of an action. An attribute has one name, can have a data type, can be (or not) mutable (i.e., modifiable by customers), can be (or not) required (i.e., value is provided at creation time), can have a default value and a human-readable description.

• AnnotatedElement is an added concept to represent the abstract base class inherited by Attribute and Category. Each attribute/kind/mixin/action can own zero or more annotations.

• Annotation is an added concept and represents an additional information that can be attached to an AnnotatedElement instance. This mechanism is usually used to limit changing the metamodel. It allows us adding an information that may not be related to the core of the OCCI specifications, but important to some related processes like code generation, model visualization, etc.

• FSM is an added concept to model the behavior of OCCI concepts such as state diagrams of OCCI Kind instances used in both the Infrastructure [Nyrén 2016c] and Platform [START_REF] Metsch | [END_REF]] extensions. FSM describes the behavior of a kind/mixin instance, the current state is stored in a specific attribute and can own a set of states (State).

Definition 9

The type of a FSM attribute must be EnumerationType. c o n t e x t S t a t e i n v a r i a n t L i t e r a l T y p e : owningFSM . a t t r i b u t e . type= s e l f . l i t e r a l . enumerationType ;

• Transition is an added concept to represent a FSM transition from a source to a target FSM state. When a transition is triggered, an associated action is executed.

Definition 12

The action of a Transition instance must belong to the actions of the owner Type instance.

c o n t e x t T r a n s i t i o n i n v a r i a n t ActionMustBeDefined : s e l f . o c l C o n t a i n e r ( ) . oclAsType ( S t a t e ) . o c l C o n t a i n e r ( ) . oclAsType ( FSM) . o c l C o n t a i n e r ( ) . oclAsType ( Type ) . a c t i o n s ->i n c l u d e s ( s e l f . a c t i o n )

• DataType is an added concept to represent an abstract type defining OCCI data types. A DataType instance has a name and a documentation.

• BasicType is an added concept to represent an abstract type extending DataType meta-class and defining OCCI primitive data types.

• BooleanType is an added concept to represent a type extending BasicType meta-class and defining OCCI boolean data types.

• NumericType is an added concept to represent a type extending BasicType meta-class and defining OCCI numeric data types. A numeric type has a concrete type, a totalDigits value defining the maximal number of digits of a number, a minimal exclusive minExclusive value, a maximal exclusive maxExclusive value, a minimal inclusive minInclusive value, and a maximal inclusive maxInclusive value.

• NumericTypeEnum is an added concept to represent an enumeration type defining the different OCCIware concrete numeric types. A NumericType can be Byte, Double, Float, Integer, Long, Short, or BigDecimal.

• StringType is an added concept to represent a type extending BasicType meta-class and defining OCCIware string data types. A StringType instance can have a pattern value defining a pattern constraint expressed as a regular expression, a length value defining a length constraint, a minLength value defining the minimum length constraint, and a maxLength defining the maximum length constraint.

• EObjectType is an added concept to represent a type extending BasicType meta-class and defining OCCIware Java data types such as URI, Date, etc.

• ArrayType is an added concept to represent array data types. An ArrayType instance has a type defining its type.

• EnumerationType is an added concept to represent enumeration data types.

An EnumerationType instance owns a set of literals.

• EnumerationLiteral is an added concept to represent an enumeration literal.

An EnumerationLiteral instance has a name and a documentation.

• RecordType is an added concept to represent record data types. A RecordType instance owns a set of record fields (recordFields).

• RecordField is an added concept to represent a record field. It extends the Attribute meta-class.

• Integer is an Ecore data type defining the primitive Integer type.

• Boolean is an added concept to represent an Ecore data type defining the primitive Boolean type.

• String is an added concept to represent an Ecore data type defining the primitive String type.

• URI is an added concept to represent an Ecore string-based data type extended with a pattern constraint that conforms to the Uniform Resource Name (URN) syntax [Moats 1998].

• Name is an added concept to represent an Ecore string-based data type extended with the following pattern "[a-zA-Z][a-zA-Z0-9_-]*". This data type allows us to initialize a valid name attribute to the OCCI constructs and, thus, deduce a term conforms to the OCCI RESTful HTTP Rendering specification [Nyrén 2016a].

• AttributeName is an added concept to represent an Ecore string-based data type extended with the following pattern "[a-zA-Z0-9]+(\.[a-zA-Z0-9]+)+". It allows us to create AttributeName instances conform to the OCCI Text Rendering specification [Edmonds 2016].

• Scheme is an added concept to represent an Ecore string-based data type extended with a pattern constraint conforms to the Uniform Resource Identifier (URI) syntax [Berners- Lee 1998].

• OCL is an added concept to represent an Ecore string-based data type allowing us to create correct OCL expressions.

• Configuration is an added concept to represent a running OCCI system.

Configuration owns zero or more resources (and transitively links), and use zero or more extensions. For a given configuration, the kind and mixins of all its entities (resources and links) must be defined by used extensions only. This avoids a configuration to transitively reference a type defined we do not know where.

Definition 13

The kind of all resources of a configuration must be defined by an extension that is explicitly used by this configuration. • Link is an OCCI Core Model concept and represents a relation between two resources, such as a virtual machine connected to a network and an application hosted by a virtual machine. A Link instance refers to both a source and target resource.

Definition 16

The kind of a Link instance must inherit from the link kind instance directly or transitively. • Entity is an OCCI Core Model abstract concept. Each OCCI entity (resource or link) owns zero or more attributes, such as its unique identifier, the host name of a virtual machine, the Internet Protocol address of a network. In addition, each OCCI entity is strongly typed by a Kind and a set of Mixin instances. As OCCI is a REST API, it gives access to cloud resources via classical CRUD operations (i.e., Create, Retrieve, Update, and Delete).

Definition 17 The kind of an Entity instance must be compatible with one applies kind instance of each mixin parts of this entity. • AttributeState is an added concept to represent an instantiated OCCI attribute. An AttributeState instance has a name and a value.

• MixinBase is an added concept strongly typed by a mixin. It represents an instantiated mixin and allows us to instantiate the attributes of the referenced mixin outside the owner entity in order to separate the entity attributes from the mixin ones. A MixinBase can own zero or more attributes.

OCCIware Studio

Once the OCCIware Metamodel was defined, it has been tooled with OCCIware Studio, which is a set of plugins for the Eclipse [ecl] IDE. Figure 3.7 shows all the main features of OCCIware Studio: • OCCIware Designer is a graphical modeler to create, modify, and visualize both OCCI extensions and configurations. The OCCI standard does not define any standard notation for the graphical or textual concrete syntax. This tool is implemented on top of the Eclipse Sirius framework [sir].

• OCCIware Editor is a textual editor for both OCCI extensions and configurations. Our OCCI textual syntax is described in [Merle 2015b]. This tool is implemented on top of the Eclipse Xtext framework [xte 2016].

• OCCIware Validator is a tool to validate both OCCI extensions and configurations. This tool checks all the constraints defined in the OCCIware Metamodel, i.e., both Ecore and OCL ones.

• Textile Documentation Generator is a tool to generate a Textile documentation from an OCCI extension model. Textile is a Wiki-like format used for instance by GitHub projects. This tool is implemented on top of the Eclipse Acceleo framework [acc].

• Latex Documentation Generator is a tool to generate a Latex documentation from an OCCI extension model. It allows us to later generate a portable document describing the OCCI extension. This tool is implemented on top of the Eclipse Acceleo framework.

• Ecore Generator is a tool to generate the Ecore metamodel and its associated Java-based implementation code from an OCCI extension. As shown in the left part of The main goal of our work consists in introducing a tooled framework, based on OCCI, that manages any kind of resources as a service.

To do that, it was necessary to map different OCCI concepts into a modeling framework to benefit from the available facilities for building tools based on a metamodel (the right part of Figure 3.8). EMF was chosen to embed OCCI and, thus, the OCCIware Metamodel was proposed as a precise meta-model for OCCI [Merle 2015a]. Therefore, we can define either an OCCI extension model or an OCCI configuration model that conform to the OCCIware Metamodel. However, the current tooling in EMF does not allow us to encode that: an OCCI configuration is an "instantiation" of an OCCI extension. For that, OCCIware proposes, using the Ecore Generator tool, to promote the OCCI extension model by translating it into an Ecore metamodel, extending the OCCIware Metamodel. Consequently, we can design an Extension configuration model, instance of this generated metamodel. Later, we can deduce a semantically equivalent OCCI configuration model, instance of the OCCIware Metamodel.

This tool is directly implemented in Java. In the following, the generation process of OCCIware Metamodel concepts into the EMF concepts is detailed:

-Each OCCI kind instance is translated into an Ecore class. If its parent is the Resource kind, the generated class extends the Resource Ecore class of the OCCIware Metamodel. Otherwise, if its parent is the Link kind, the generated class extends the Link Ecore class of the OC-CIware Metamodel.

-Each OCCI mixin instance is translated into an Ecore class extending the MixinBase class of the OCCIware Metamodel.

-Each OCCI attribute instance, owned by an OCCI kind/mixin, is translated into an Ecore attribute owned by the corresponding generated Ecore class.

-Each OCCI action instance, owned by an OCCI kind/ mixin, is translated into an Ecore operation owned by the corresponding generated Ecore class.

-Each OCCI constraint instance is translated into an OCL invariant.

-All Ecore data types defined in the OCCI extension are translated into the corresponding EMF concepts and/or types in the generated OCCI extension metamodel.

Table 3.1 outlines the mapping process of OCCIware Metamodel concepts into EMF concepts.

• Alloy Generator is a tool to generate an Alloy specification from an OCCI extension model. Alloy is a lightweight formal specification language based on the first-order relational logic [Jackson 2012]. We are able to analyze OCCI The generated OCCI configurations can be displayed graphically with the OCCIware Designer. Alloy Generator is the core of the fclouds approach, my contribution that I detail in Chapter 5. This tool is implemented on top of the Eclipse Acceleo framework.

• Connector Generator is a tool to generate the OCCI connector implementation associated to an OCCI extension. This generated connector code extends the generated Ecore implementation code. This connector code must be completed by software developers to implement concretely how OCCI CRUD operations and the specific actions must be executed on a real cloud infrastructure. Later, this generated connector will be deployed on OCCIware Runtime. This tool is implemented on top of the Eclipse Acceleo framework.

• Designer Generator is a tool to generate a graphical extension-specific designer from an OCCI extension. This designer can be later customized to be able to represent the concepts related to the extension domain. This tool is implemented on top of the Eclipse Acceleo framework and generate Eclipse Sirius models.

• CURL Generator is a tool to generate a CURL-based script from an OCCI configuration model. These generated scripts contain HTTP requests to instantiate OCCI entities into any OCCI-compliant runtime. These scripts are used for offline deployment. This tool is implemented on top of the Eclipse 3.6. OCCIware Runtime Acceleo framework.

• Runtime Connector is a tool to synchronize OCCI configuration models with running OCCI configurations hosted by any OCCI-compliant runtime. This connector allows cloud developers to introspect an OCCI runtime in order to build the corresponding OCCI configuration model, then update this model and send changes back to the OCCI runtime. This tool integrates the jOCCI API4 , a Java library implementing transport functions for rendered OCCI queries.

• Configuration Converter is a tool to translate an Extension configuration model into an OCCI configuration model (the equivalent relation in Figure 3.8). This tool allows us to reuse the tools specific to OCCI artifacts such as the CURL Generator to deploy later the configuration into an OCCIcompliant runtime. This tool is directly implemented in Java.

OCCIware Runtime

To enact OCCI configuration models, we adopt the Models@run.time approach [START_REF] Blair | [END_REF]] that extends the use of modeling techniques beyond the design and implementation phases. It seeks to extend the applicability of models and abstractions to capture the behavior of the executing environment. End users of OCCIware Studio require interaction with cloud APIs to create, retrieve, update and delete cloud resources. Therefore, OCCIware Runtime is implemented as a generic Java implementation of OCCI, available as an open-source project5 . The OCCIware Runtime can be deployed as a standalone server including an embedded Jetty server or as a Java library that is based on Java Servlet API specification.

The OCCIware Runtime is composed of four main parts, as illustrated in Figure 3.9.

• OCCI Server that implements the following OCCI specifications: Users send their HTTP requests to the OCCIware Runtime to manage an OCCI configuration and wait for a reply. In the OCCIware Runtime, the processing of a user's request consists of managing the OCCI HTTP protocol, decoding the HTTP request body according to its text or JSON format, forwarding the request to the OCCI Core Model, controlling if the request is allowed by the OCCIware extension, calling the connector related to the targeted cloud API, preparing the request to send to the cloud provider, communicating with the cloud API via its associated network protocol, processing the request by the cloud provider, encoding the HTTP reply body, and return the reply to the user. Then the user processes the reply.

Evaluation of OCCIware Studio

This section validates the OCCIware approach. We discuss how OCCIware addresses the different requirements listed in Section 3.1. At first, we show the different OCCI extensions defined by the OGF's OCCI working group and implemented with

OCCIware. We particularly focus on the Infrastructure extension by showing how the cloud developer leverages the generated tooling around this extension to create/manage his/her configuration models with OCCIware Studio and deploy them in the cloud. Then, we illustrate the different OCCIware approach usages presented in Section 3.3 by presenting five major use cases that apply OCCIware.

Implementation of a Catalog of Standard OGF's OCCI Extensions

Each OCCI extension is implemented as an Eclipse modeling project containing one extension model, which is an instance of OCCIware Metamodel. Currently, OCCIware Studio supports the five OCCI extensions defined by the OGF's OCCI working group.

The OCCI Infrastructure Extension

OCCI Infrastructure [Nyrén 2016c] defines compute, storage and network resource types and associated links. To design the Infrastructure extension, the OCCI-Resources with OCCIware ware architect can use OCCIware Designer and/or OCCIware Editor. This extension defines five kinds (Network, Compute, Storage, StorageLink and NetworkInterface), six mixins (Resource_Tpl, IpNetwork, Os_Tpl, SSH_key, User_Data, and IpNetworkInterface), and around twenty data types (Vlan range, Architecture enumeration, various status enumerations, etc.). Figure 3.10 shows a subset of this extension. The complete one is available here7 . The Compute kind represents a generic information processing resource, e.g., a virtual machine or container. It inherits the Resource defined in the OCCI Core extension. It has a set of OCCI attributes such as occi.compute.architecture to specify the CPU architecture of the instance, occi.compute.core to define the number of virtual CPU cores assigned to the instance, occi.compute.memory to define the maximum RAM in gigabytes allocated to the instance, etc. The Compute kind exposes five actions: start, stop, restart, save and suspend.

The Network kind is an interconnection resource and represents a Layer 2 (L2) networking resource. This is complemented by the IpNetwork mixin. It exposes two actions: up and down.

The orange-colored box in Figure 3.10 illustrates the state diagram of a Network instance and describes its behavior. As shown previously in Section 3.4, the OCCIware Metamodel provides the required concepts to describe the behavior of each kind/mixin. In addition, it allows us defining extension-specific constraints. For i f ( t r u e ) { // TODO: T r a n s i t i o n a c t i v e -down-> i n a c t i v e s e t S t a t e ( NetworkStatus . INACTIVE) ; } e l s e { // TODO: T r a n s i t i o n a c t i v e -down-> e r r o r s e t S t a t e ( NetworkStatus .ERROR) ; } } } } Listing 3.1: The Generated Network Connector Class.

Once the generation step is achieved, the software developer can complete the generated connector classes by updating their methods implementations (TODO sections in Listing 3.1) with business code related to targeted API. For the NetworkConnector class, the software developer completes the code to trigger that the OCCI Network resource was created (occiCreate), will be retrieved (occiRetrieve), was updated (occiUpdate) and will be deleted (occiDelete). In addition, he/she completes the generated methods (up and down) related to specific actions defined in the Network kind. The completed connector code must be later deployed on the OCCIware Runtime. Then, the software developer can proceed to the customization of the generated Infrastructure Designer which will be used to create Infrastructure configuration models as shown in Figure 3.11. From now on, we can consider that the OCCI Infrastructure extension is completely tooled and able to be used to manage conforming configurations.

Using OCCIware Studio enriched with the Infrastructure Tooling, cloud developers can design an OCCI Infrastructure configuration model conforms to the Infrastructure Metamodel. Figure 3.11 illustrates a small infrastructure configuration composed of a compute (vm1) connected to a network (network1), via an OCCI link (green-colored box), the network interface (ni1). As this configuration uses an IP-based network, the Network resource and the NetworkInterface link have an IpNetwork and IpNetworkInterface mixin, respectively. Each OCCI entity is configured by its attributes, e.g., vm1 has the vm1 hostname, an x64-based architecture, 4 cores, and 4 GiB of memory.

To benefit from the OCCI-compliant tools defined in the OCCIware Studio, an Infrastructure configuration model must be translated into an OCCI configuration model that conforms to the OCCIware Metamodel. In order to deploy and manage the generated OCCI configuration models, cloud developers interact with the cloud by sending OCCI HTTP requests to OCCIware Runtime. These requests can be automatically generated as CURL scripts using the CURL Generator tool. Listing 3.2 shows the CURL script that requests OC-CIware Runtime via both OCCI HTTP Protocol [Nyrén 2016a] and OCCI Text Rendering [Edmonds 2016] to create the network1 instance. Then, OCCIware Runtime invokes the occiCreate() method of the NetworkConnector class, which implements how to create the considered network instance in the cloud. Finally, the Listing 3.2: The generated CURL script to create a Network instance The proposed tooling around the OCCI Infrastructure extension allows us, with our industrial partner Scalair [scaa], to implement a Java connector for VMware API. The whole tooling around Infrastructure extension is available here8 . In the future, we will target additional CRM-APIs such as AWS, OpenStack, GCP, etc.

The OCCI CRTP Extension

OCCI CRTP [START_REF] Drescher | [END_REF]] defines a set of preconfigured instances of the OCCI compute resource type. It extends the Infrastructure extension. Figure 3.13 shows the OCCI CRTP extension designed with OCCIware Studio. Its tooling is available here9 .

The OCCI Platform Extension

OCCI Platform [START_REF] Metsch | [END_REF]] defines application and component resource types and associated links. Figure 3.14 shows the OCCI Platform extension designed with OCCIware Studio. Its tooling is available here10 .

The OCCI Monitoring Extension

OCCI Monitoring [START_REF] Ciuffoletti | Open Cloud Computing Interface -Monitoring Extension[END_REF]] is a draft specification and defines sensor and collector types for monitoring cloud systems. Figure 3.16 shows the OCCI Monitoring extension designed with OCCIware Studio. Its tooling is available here12 .

Five OCCIware Use Cases

In this subsection, five major use cases of the OCCIware approach are illustrated.

Cloud Simulation with OCCIware

This work [Ahmed-Nacer 2016a, Ahmed-Nacer 2017] provides a methodology for the simulation of OCCI configurations. The simulation technology has increasingly become popular as it allows users to evaluate their algorithms and applications before deploying them on a real cloud environment. This work reuses CloudSim [Calheiros 2011], a generalized and extensible simulation framework that allows seamless modeling, simulation, and experimentation of emerging cloud computing infrastructures and application services. CloudSim allows users to test the performance of a newly developed application service in a controlled environment. Moreover, CloudSim allows a user to model and simulate all the cloud infrastructure resources. The main idea of this use case consists in defining an OCCI extension named Simulation which extends the Infrastructure extension. The extension defines two notions: a resource to simulate represents the resource to be simulated, and a simulation resource represents the resource which performs the simulation activity. Two main artifacts are generated for this use case: Simulation Metamodel and Simulation Designer. Once a Simulation configuration model is defined, it can be later verified, and analyzed by the CloudSim tool. The simulation activity evaluates the configuration using some metrics such as the percentage of used These requests may be: creating a mobile robot resource, updating its attributes, and executing an action of a mobile robot. In this work, an evaluation to measure the performance, stability, and scalability of the OMCRI has been performed. Evaluation tests have shown that OMCRI overhead remains low and that OMCRI does not add any latency. Figure 3.17 shows an OMCRI configuration modeled using the customized OMCRI Designer.

Figure 3.17: OMCRI Designer.

Docker Management with OCCIware

In this work [START_REF] Paraiso | Model-driven Management of Docker Containers[END_REF]], authors present a model-driven management of Docker [doc] containers based on OCCIware Studio. Docker is a technology used for developing, deploying and executing applications packaged into containers. Docker lacks of deployability verification tool for containers at design time. In addition, the synchronization between the designed containers and those deployed was still a major challenge for the Docker technology. Finally, Docker did not provide a mechanism to reconfigure the container resources at runtime. To resolve these issues, authors refer to the OCCIware approach by proposing Docker Studio13 , an OCCI-based studio for the Docker technology. This work defines a Docker extension using OCCIware Studio. To resolve the lack of verification challenge in Docker, this work reuses the Constraint concept added in the OCCIware Metamodel to define constraints specific to the Docker domain such as the not permitted bidirectional or closed loop link between Docker Containers. By defining this kind of information and validating it using the OCCIware Validator, the end user is now sure that his/her designed configuration is correct and it is ready to be deployed. Then, a Docker Designer is generated and customized to provide a high-level abstraction for Docker containers that is used for reasoning and managing large container deployments in the cloud. As shown in Figure 3.18, Docker Designer allows representing a human understandable description of some aspects of a running Docker system. In addition, to resolve the synchronization issue, a specific generator for the Docker technology has been provided in order to generate Docker artifacts (Docker Command-Line Interface (CLI) commands, Docker Compose file, Docker Swarm configurations). These generated artifacts are used for online deployment. Moreover, to ensure the synchronization from the running system to the Docker model, a Docker Connector has been developed. This connector updates the model elements according to the running system changes. Finally, to ensure the resource management at runtime, the developed connector implements the observer/listener design pattern. Therefore, the connector relies on a notification mechanism that reports events when a model element has been changed.

Managing Cloud Applications with OCCIware

In this work [START_REF] Korte | [END_REF]], authors focus on modeling cloud applications with OCCI. OGF defines extensions that target the requirements of different cloud service levels, such as IaaS and PaaS. However, no concrete use cases and implementations have been provided around the OCCI Platform extension. This behavior is due to several issues. At first, the lifecycle for the Component and Application resources as defined in the OCCI Platform specification is incomplete (P1 issue). Moreover, the OGF provides two separate OCCI extensions for the Infrastructure and Platform domains, but it misses to define the connection between them (P2 issue). In addition,

Synthesis on the OCCIware Approach

The OCCIware approach has been successfully applied in different use cases and domains. Each one implements some required features in a cloud modeling framework. Table 3.2 states an overview on the implementation of these usages in different use cases.

For the Infrastructure use case (Subsection 3.7.1.1), cloud architects have taken advantage of the OCCIware Studio tools to design the structural and behavioral aspects of the extension, verify it according to the requirements specific to the domain, and generate its documentation 14 . To deploy designed configurations, Infrastructure use case implements the code generation strategy to pro-Chapter 3. Modeling, Verifying, Generating and Managing Cloud Resources with OCCIware duce CURL scripts from an OCCI configuration. In addition, model interpretation strategy is also implemented. Indeed, an OCCI extension for the VMware technology has been defined15 . VMware extension extends the Infrastructure extension. A VMware connector has been developed. It supports the deployment of a designed VMware configuration in the cloud environment. In addition, it ensures the reconfiguration of a running system at runtime (management) and the synchronization between the design and the execution environment by affecting changes occurred in the executing environment to the existing architecture (monitoring).

For the Cloud Simulation use case (Subsection 3.7.2.1), it illustrates several usages of the OCCIware approach. At first, it represents the capability to create a specific designer for the Simulation domain. In addition, it shows how we can come back from the Simulation Studio to the OCCIware Studio by generating an OCCI configuration model from a Simulation configuration model. Finally, this work implements the model interpretation strategy by simulating an OCCI configuration model using the CloudSim API. This use case illustrates how we can plug an external API, here CloudSim, into the OCCIware framework. In fact, once a configuration has been designed, it can be reused for several activities such as simulation, deployment, and cost analysis.

OMCRI use case (Subsection 3.7.2.2) endorses the fact that we can manage XaaS with the OCCIware approach, even mobile robots. OMCRI use case validates the genericity of the OCCIware Runtime. In addition, the evaluation shows that adopting the OCCIware approach into another domain, other than cloud computing, does not cause a latency that damages the responsiveness of the system. Docker use case (Subsection 3.7.2.3) is considered as the first OCCI-based studio implemented with OCCIware technology. It illustrates our approach to consider OCCIware as a factory to build cloud modeling frameworks (right part of Figure 3.5). Docker Studio represents a concrete use case which implements both strategies, code generation, and model interpretation, to execute designed models specific to a particular domain. The most important feature developed in the Docker use case is the mapping of a running architecture from the execution environment to the modeling framework. It allows end users to benefit from the Docker Studio while the configuration was not initially designed using it.

MoDMaCAO use case (Subsection 3.7.2.4) validates the applicability of the OC-CIware approach on different cloud layers. This work is the result of a fruitful collaboration between the OCCIware team in Inria, Spirals, Fabian Korte and Jens Grabowski from the University of Goettingen. MoDMaCAO can even be applied to connect two layers in the cloud such as IaaS and PaaS. Model interpretation strategy has been experimented by developing a connector which allows us to deploy and manage different designed cloud applications using Ansible [ans], a flexible configuration management system. Code generation strategy may also be experimented by generating Ansible playbook artifacts from MoDMaCAO configurations.

GCP use case (Subsection 3.7.2.5) represents the first use case that applies the OCCIware approach on a big cloud provider, a.k.a GCP. I present the GCP use case in the next chapter. GCP use case is a major part of my first contribution in this thesis. In this work I target to integrate both code generation and model interpretation strategies. With the code generation approach, they aim to use GCP configurations to generate GCP artifacts, such as JSON files that contain the needed structured information for creating a VM for example. In addition, this use case aims to experiment the model interpretation approach, by defining the business logic of GCP connector which defines the relationship between GCP configurations and their executing environment.

To summarize, the OCCIware approach provides a software product line, named OCCIware Studio Product Line as shown in Figure 3.20. OCCIware Studio is considered as a factory to create other studios. Each one targets a particular cloud domain. The different generated studios share a common base, which is OCCIware Metamodel. Therefore, composing the different generated studios can be an interesting perspective to create an Internet of Everything (IoE) Studio that allows us to compose heterogeneous concepts and domains in the same modeling framework. Resources with OCCIware

Summary

This chapter presented OCCIware, the first model-driven approach for OCCI. The OCCIware approach provides two main components: OCCIware Studio and OCCIware Runtime. OCCIware Studio is a model-driven tool chain to design OCCI artifacts. It is built on the top of a metamodel, named OCCIware Metamodel, which defines the precise semantics of OCCI in Ecore and OCL. Our metamodel can be seen as a DSML to define and exchange OCCI extensions and configurations between end users and resource providers. OCCIware Runtime is a generic OCCI-compliant runtime environment.

The OCCIware approach is proposed as a framework to manage XaaS with OCCI. Moreover, the OCCIware approach is considered as a factory of cloud domain-specific modeling languages and studios due to its capability to generate a complete framework to manage resources specific to a particular cloud domain. The OCCIware approach has been validated via several use cases, which target different domains (IaaS, PaaS, RaaS and CaaS). Each use case illustrates a specific usage of the OCCIware approach and demonstrates its genericity and extensibility.

In the next part of this dissertation, I present my contributions that are based on the OCCIware approach. In the next chapter, I present my approach for representing in an enhanced and automated way the concrete set of cloud concepts and the behaviour of cloud operations. Documentations lack of verification process that ensures the correctness of cloud configurations before their deployment. Cloud models play an important role to capture the expectations of a cloud API and to a priori validate the correctness of its cloud configurations. These models are manually designed so far, which is prohibitively labor intensive, time consuming and error-prone. To address this issue, I propose a novel approach to infer model-driven specifications from natural language text of cloud API documentations. My approach is applied on a concrete cloud provider, GCP, which is today one of the most important and growing provider in the cloud market. GCP provides developers several products to build a range of programs from simple websites to complex applications. Although it was established only five years ago, GCP has gained notable expansion due its suite of public cloud services that it based on a huge, solid infrastructure. Actually, GCP offers hosting services on the same supporting infrastructure that Google uses internally for end-user products like Google Search and YouTube. This outstanding reliability results in GCP being adopted by eminent organizations such as Airbus, Coca-Cola, HTC, Spotify, etc. In addition, the number of GCP partners has also increased substantially, most notably Equinix, Intel and Red Hat.

To use GCP services, expert developers refer at first to the GCP API documentation provided at GCP website. By going through the GCP documentation, I realize that it contains wealthy information about GCP services and operations, such as the semantics of each attribute and the behaviour of each operation. However, GCP documentation is described through HTML pages at its website1 and is written in natural language, a.k.a. English prose, which results in human errors and/or semantic confusions. Also, the current GCP documentation lacks of visual support, hence the developer will spend considerable time before figuring out the links between GCP resources. To avoid confusion and misunderstandings, the cloud developers obviously need a precise specification of the knowledge and activities in GCP.

After presenting the general approach we promote to obtain formal cloud models, this chapter presents a precise model for GCP. It describes GCP resources and operations, reasons about this API and provides corrections to its current drawbacks, such as Informal Heterogeneous Documentation, Imprecise Types, Implicit Attribute Metadata, Hidden Links, Redundancy and Lack of Visual Support that I detail in Section 4.2. This is a work of reverse engineering [START_REF] Rugaber | Model-Driven Reverse Engineering[END_REF]], which is the process of extracting knowledge from a man-made documentation and reproducing it based on the extracted information. In order to formally encode the GCP API without ambiguity, I choose to automatically infer a GCP Model as the target documentation format. In fact, my approach leverages the use of MDE to provide a precise and homogeneous specification, and reduce the cost of developing complex systems. MDE allows to rise in abstraction from the implementation level to the model level, and to provide a graphical output and a formal verification of GCP structure and operations. My GCP Model conforms to the OCCIware Metamodel presented in Chapter 3.

The contributions of this chapter can be summarized in three categories:

1. an automated approach to infer models from textual documentations, 2. a concrete use case of our approach: a precise GCP Model that consists in a formal specification of GCP. This model, automatically built, also provides corrections for the drawbacks that I identified in GCP documentation,

3. an analysis of GCP documentation because it is as important as analyzing the API itself. This is done thanks to my model which is a clearer representation of GCP compared to the original one and hence easier to reason over it, and, 4. a validation of the preciseness of my GCP model.

This chapter is structured as follows. Section 4.1 argues for the need to analyze cloud textual documentations and proposes a protocol to automatically infer models from them. Section 4.2 identifies six general drawbacks of GCP documentation that motivate this work. Next, Section 4.3 describes my model-driven approach for a better description of GCP API and gives an overview of some background concepts I use in my GCP Model. Section 4.4 presents and discusses my results, which validate my approach. Finally, Section 4.5 concludes the chapter with future work.

Inferring Precise Cloud Models

Modeling cloud APIs is an important way for capturing their requirements and succeeding a thorough understanding of their behavior. Modeling allows the cloud developer to keep the cloud concepts clean from the details of implementation classes and the HTTP requests. Moreover, modeling by using MDE principles allows the developer to generate from the cloud model the corresponding Java implementation classes. The model can also be used to generate different outputs, e.g., HTML pages, or it can be interpreted at runtime by software. However, modeling the cloud requires knowledge in modeling techniques which is not necessarily available among cloud experts. For this reason, modeling experts are employed to formalize models within an iterative way in collaboration with cloud experts. This procedure involves long meetings due to ambiguities or misunderstandings among the involved actors, so the acquisition of cloud models consumes a lot of time and cannot follow-up with the extensive documentations provided by the cloud providers. These documentations are the most relevant source of information for the construction of cloud models. Such textual documents can be stored in a structured way like HTML pages, JSON, YAML or XML files or in an unstructured way like reports or manuals. However, the textual documentations may contain syntactical or semantic errors that distort the real semantics of cloud APIs and that require analysis and rectifications before gathering the information. Therefore, the acquisition process of cloud models remains relatively error-prone and costly.

To address this challenge, I propose to automatically provide a precise model of the cloud API from the documentation supplied by the cloud provider. This way, the cloud developer can easily access the model-based documentation of the cloud that he/she uses. Model-based documentations allow the developer to thoroughly understand the insights of the cloud API. I combined both web crawling and Natural Language Processing (NLP) in order to correctly infer models from the cloud documentations. The global approach is summarized as follows. First, using a dedicated web crawler, I extract information that allows me to build a model. Web crawlers are bots that visit the internet to extract information from web pages. Second, I apply NLP [Chowdhury 2003] with rules to extract properties, semantics and constraints on the API. NLP is a branch of the artificial intelligence field that automates the study and extraction of useful knowledge from texts written by humans, in order to better interface with computers. In this context, programs implementing NLP take as input a text flow and exploit information to achieve several tasks such as relationship extraction, automatic summarization, terminology extraction, etc. NLP has two main approaches: rule-based and statistical. The former refers to the idea of using hand-coded set of rules to exploit information. For instance, to recognize email addresses, IP addresses, I use specific regular expressions. This approach is easy to implement and suitable for specific cases. The latter relies on machine learning to achieve more complex tasks. My approach exploited the rule-based NLP which successfully achieved knowledge extraction. My web crawler takes into assumption the structure of the provided documentation, whether it takes the form of HTML pages, JSON files or others. Since most of cloud documentations are provided as HTML pages at the provider's website, I specifically propose in this chapter to automate the extraction of precise models from HTML cloud documentations.

Approach Overview

This section discusses the design of our approach, which is represented in • Specific Parser: First, I connect to the main page of the cloud documentation and the specific parser takes the documentation in a structured HTML format as input and extracts resources from the HTML tags. More specifically, using an HTML parser, I retrieve the table or the list containing the cloud resources. In fact, the retrieval of information from HTML pages requires recognition rules that are specific to the documentation format. Sometimes, the information is structured in tables with specific IDs. Other documentations could be organized within lists and therefore crawling must be adapted. Afterwards, for each resource, the parser retrieves the resource elements such as its name, description, list of actions and list of attributes. For each attribute, I retrieve its properties like its name, description and type.

• Model Generator: I define exhaustive and systematic mapping between the parsed cloud API concepts and the used cloud metamodel. For example, for each row of the documentation HTML table (<tr> </tr>), I add a new resource instance to the target cloud model. This resource instantiates the corresponding concept of the cloud metamodel, in terms of the mapping rules I defined. For each cell (<td> </td>) that contains the definition of an element of this resource, I add a new attribute instance to the target cloud model.

• Text Analysis Engine: Later on, the text analysis engine performs some natural language post-processing actions. I mainly define a set of rules on the description of the attributes to detect implicit properties that are not clearly stated in specific cells and to elucidate domain-specific metadata. I also apply on the description a set of rules based on keywords of each attribute to refine its type if necessary. Sometimes, the type and the description of an attribute do not match, and thus the cloud developer may define incorrect types in Documentations their HTTP requests. I also use NLP to generate a tree structure to identify relations between concepts.

• Model Validator: Finally, the cloud model I generated is passed to the model validator to ensure that it is consistent, conforms to the metamodel and behaves as expected. At each time an error is detected, I iterate on the model to fix it by defining additional rules or correcting the existing ones. Our approach does not provide automated correction mechanisms for the errors raised at the validation, the developer has to correct errors by himself/herself.

This contribution is original and striking, and I estimate that it will leave an impact in the cloud domain. It might seem simple but it involves many complicated details. In the remaining of this chapter, I apply my model inferring approach to a real and significant cloud provider and I cover the whole modeling of his documentation. I concretely exploit this idea by automatically inferring from GCP textual documentation, a precise model that conforms to the OCCIware Metamodel. This use case might be applied to other source platforms, like Amazon, towards other target platforms, like CloudML. I chose GCP because it is one of the major cloud providers with an informal documentation and OCCIware because it consists in the context of this thesis and the OCCIware Metamodel is extensible in a way to support all kinds of cloud resources.

Related Work

The literature of model-driven approaches for the cloud shows that researchers do not discuss the details of how they obtain their models for the cloud. This is due to cloud models being manually constructed. Even though researchers might have already thought about automating the process of designing cloud models, this idea has not been put into practice. To the best of our knowledge, we provide the first work that investigates and formalizes a cloud API documentation. In [START_REF] Petrillo | [END_REF]], Petrillo et al. have focused on studying three different cloud APIs and proposed a catalog of seventy-three best practices for designing REST APIs. In contrast to our work, this work is limited to analyzing the documentations of these APIs and does not propose any corrections. Two recent works were interested in studying REST APIs in general. [START_REF] Haupt | [END_REF]] provides a framework to analyze the structure of REST APIs to study their structural characteristics, based on their Swagger documentations. [START_REF] Cao | [END_REF]] presents AutoREST, an approach and a prototype to automatically infer an OpenAPI specification from a REST API HTML documentation. Our work can be seen as a combination of these two previous works [START_REF] Haupt | [END_REF][START_REF] Cao | [END_REF]], since we infer a rigorous model-driven specification from GCP HTML documentation and we provide some analysis of its corresponding API. However, in contrast to these two works, our work is specifically applied on a cloud REST API and proposes corrections to the detected deficits of its documentation. Moreover, given that it is an important but very challenging problem, analyzing natural language documents from different fields has been studied by many previous works. In [Zhai 2016], Zhai et al. apply NLP techniques to construct models from Javadocs in natural language. These models allow one to reason about library behaviour and were implemented to effectively model 326 Java API functions. [START_REF] Pandita | [END_REF]] presents an approach for inferring formal specifications from API documents targeted towards code contract generation. [START_REF] Zhong | [END_REF]] develops an API usage mining framework and its supporting tool called Mining API usage Pattern from Open source repositories (MAPO) for mining API usage patterns automatically. [START_REF] Sinha | [END_REF] proposes abstract models of quality use cases by inspecting information in use case text.

GCP Use Case: Motivation & Drawbacks

The object of my study is the GCP documentation. GCP is a proprietary cloud platform that consists of a set of physical assets (e.g., computers and hard disk drives) and virtual resources (e.g., virtual machines, a.k.a. VMs) hosted in Google's data centers around the globe. I especially target this API because it belongs to a well-known cloud provider and because I believe it can be represented within a better formal specification.

GCP documentation is available in the form of HTML pages online. The URL2 is the starting point of my study and the base for building my GCP Model. This page exhaustively lists the resources supported by the deployment manager, and provides a hyperlink to each of these resources. Normally, the developer will use the deployment manager to deploy his/her applications. The deployment manager will then provision the required resources. Therefore, I adopt this page to study the documentation of each GCP resource that could be provisioned by the developer.

Through my study of GCP, I have identified six main conceptual drawbacks/limitations on GCP documentation, which are detailed below.

Informal heterogeneous documentation. Enforcing compliance to documentation guidelines requires specialized training and a strongly managed documentation process. However, often due to aggressive development schedules, developers Chapter 4. Inferring Precise Models from Cloud APIs Textual Documentations neglect these extensive processes and end up writing documentations in an ad-hoc manner with some little guidance. This results in poor quality documentations that are rarely fit for any downstream software activities.

By going through the HTML pages of GCP documentation, it was not long before I realized that it has two different formats to describe the attributes of each resource (cf. Figure 4.2). This is an issue because it may disturb and upset the reader, i.e., the cloud developer. Imprecise types. GCP documentation is represented by a huge number of descriptive tables written in natural language. Thus it is a syntactically and semantically error-prone documentation; it may contain human-errors and its static and dynamic semantics are not well-formed, i.e., does not describe without ambiguity the API and its behavior. In fact, some of the written sentences are imprecise and can be interpreted in various different ways, which can lead to confusions and misunderstandings when the user wants to provision cloud resources from GCP API. For each resource attribute, I checked the corresponding type and description to assess whether the information is accurate. Figure 4.3 shows that the current GCP documentation states explicitly that string types are supported. But later on, further details in the description explain how to set such strings. For example, the effective type of the attribute is a URL in (1), an email address in (2), an enumer-ation in (3), and an array in (4). The cloud developer may define non-valid string formats for his/her application. The bugs will be detected during the last steps of the provisioning process and fixing them becomes a tricky and time consuming task. Implicit attribute metadata. I notice that GCP documentation contains implicit information in the attribute description. For example, it contains some information that specifies if an attribute:

• is optional or required (cf. • is mutable or immutable (cf. These constraints are only explained in the description of each attribute, but lacks of any verification process. The developer will not be able to ensure, before the deployment phase, that his/her code meets these constraints.

Hidden links. A link is the relationship between two resource instances: a source and a target. These links are implicit in GCP documentation but they are important for proper organization of GCP resources. They are represented by a nested hierarchy, where a resource is encompassed by another resource and where an attribute defines the link between these resources, either directly or indirectly. Figure 4.9 shows an example of a deducible link, a.k.a. networkInterface because the description of this attribute is a URL pointing to the target resource, a.k.a. network. Therefore, I can say that networkInterface is a link that connects an instance to a network. If graphical support exists, this link would definitely be more explicit. Redundancy. In addition to this, I observe from my study that GCP documentation is redundant. According to my observation, it contains a set of attributes and actions in common, i.e., with the same attribute name and type, and the same action name and type respectively. Among this set, I especially notice a redundancy of the attributes name, id, kind, selfLink, description, etc., as well as of the actions get, list, delete, insert, etc.

Lack of visual support. Finally, the information in GCP documentation is only descriptive, which involves a huge time to be properly understood and analyzed. In contrast to textual descriptions, visual diagrams help to avoid wastage of time because it easily highlights in short but catchy view the concepts of the API. Consequently, logical sequence and comparative analysis can be undertaken to enable quick understanding and attention. Cloud developers can view the graphs at a glance to understand the documentation very quickly, which is more complicated through descriptive format.

Overall, these six drawbacks above are calling for more analysis of GCP documentation and for corrections. Once the development has begun, corrections can be exponentially time consuming and expensive to amend. Therefore, the cloud developer firstly needs a clear detailed specification, with no ambiguous information, in order to:

1. make the development faster and meet expectations of the cloud API, 2. avoid the different interpretations of a functionality and minimize assumptions, and,

3. help the developer to move along more smoothly with the API updates for maintainability purpose. To understand the concepts that rely under the architecture of my approach, I begin by giving an illustration of it in Figure 4.10. This architecture is composed of three main parts: a Snapshot of GCP HTML pages, a GCP Crawler and a GCP Model increased by Model Transformations for GCP Refinement. Each of these four parts is detailed in the following.

GCP Model Extraction Approach

GCP Snapshot

Google is the master of its cloud API and its documentation, which means that GCP engineers could update/correct GCP documentation, whenever they are requested to or they feel the urge to. But since continuously following up with GCP documentation is crippling and costly, I locally save the HTML pages of GCP documentation in order to have a snapshot of GCP API at the moment of crawling its documentation. This snapshot is built on July 27, 2017.

GCP Crawler

In order to study and understand GCP documentation, the main step of my approach is to extract all GCP resources, their attributes and actions and to save them in a format that is very simple and easily readable by a human. In this sense, extracting knowledge by hand from this documentation is not reliable nor representative of reality; if the documentation changes, extracted knowledge should also evolve through an automated process. Therefore, I have set up an automatic crawler to infer my GCP specification from the natural language documentation.

GCP Model

For a better description of the GCP resources and for reasoning over them, I propose to represent the knowledge I extracted into a model that formally specifies these resources, while providing a graphical concrete syntax and processing with transformations. This addresses the drawbacks of GCP documentation identified in Section 4.2. Choosing the adequate metamodel when developing a model is crucial for its expressiveness [Fowler 2010]. In this context, a language tailored for cloud computing domain will bring us the power to easily and finely specify and validate GCP API. Therefore, I choose to adopt the OCCIware Metamodel because it is a precise metamodel dedicated to describe any kind of cloud resources. As I detailed in Chapter 3, the OCCIware Metamodel is encoded in EMF [START_REF] Steinberg | [END_REF]] and it defines its own data type classification system. Therefore, it easily allows to define primitive types such as booleans, numerics and strings, and complex types such as arrays, enumerations and records. In addition, thanks to its Extension concept, OCCIware Metamodel allows us to define a set of resource instances targeting a concrete cloud computing domain such as GCP.

In my approach, I exploit these two advantages and I build a GCP Model, which is an expressive model and an appropriate abstraction of the GCP API.

GCP Model conforms to OCCIware Metamodel, which conforms to Ecore Metamodel, as illustrated in Figure 4.11.

To go further, I present my approach with an algorithm, as illustrated in Fig- ure 4.12. First, using the OCCI API, I create a model, i.e., an OCCI extension (cf. line 1). Then, I connect to the GCP documentation using the jsoup library that provides an API to parse HTML pages from a URL (cf. line 2). Second, for each resource in the HTML page, I apply the following procedure (cf. line 3): I connect to the dedicated documentation page of the resource (cf. line 4). I create an OCCI resource (cf. line 5) and I use the information inside the HTML page to set the correct values (cf. line 6). Third, for each attribute of the resource detailed in the HTML page (cf. line 7), I extract information from the documentation and add them to the OCCI attribute (cf. line 9). The newly created attribute is added to the set of attributes of the OCCI resource (cf. line 10). Eventually, I add the new OCCI resource to the model under construction and so on (cf. line 11). In order to ease the understanding of this work, I briefly present in the following the main concepts of OCCIware Metamodel used to design my GCP Model (cf. Figure 4.13). For more details on the OCCIware Metamodel, readers can refer to Chapter 3.

• Extension represents concrete cloud computing domains, e.g., IaaS, PaaS, SaaS. In my work, Extension represents the GCP Model. It contains several kinds and data types.

• Kind represents a GCP entity type, such as version, firewall, image, instance, network, cluster, database, etc. Each Kind has a set of attributes and actions. A Kind can have as parent another Resource or Link. A Link is a relation between two Resource instances. For example, networkInterface connects a virtual machine instance to a network instance.

• Attribute represents a property of a GCP resource or a link, such as its id, name, description, selfLink, timestamp, etc. An Attribute instance has a name, a description, may have a default value and may be mutable or required.

• Action represents an operation that can be executed on GCP API, i.e., on its Kind instances, such as create an instance, get a database, delete a cluster, etc.

• BooleanType represents the Boolean type. For example, the vm attribute expects a boolean value to indicate whether to deploy a version on a virtual machine or in a container and the autoDelete attribute to denote whether the disk will be auto-deleted when the instance is deleted.

• NumericType represents numeric types such as Byte, Double, Float, Integer, Long, Short, etc., as well as their minimal and maximal values. For example, the currentDiskSize attribute, which is the current disk usage of a Cloud SQL resource, expects a long type value and the targetUtilization attribute, which is the target CPU utilization to maintain when scaling, expects a float type value between 0 and 1.

• StringType represents string types, as well as their regular expressions if they exist. A regular expression is used to define the specific textual syntax for representing patterns that matching text needs to be conform to. For example, the networkIP attribute, which is an IPv4 internal network address to assign to a network interface of an instance resource, expects a string type value with an appropriate regular expression to check for an IP address.

• ArrayType represents a complex DataType to define lists and their types. For example, the serverNames attribute, which is list of server names that are delegated to a managed zone, is an array of strings.

• EnumerationType represents a complex DataType to define enumerations.

Each EnumerationType has at least one literal (EnumerationLiteral). For example, the status attribute of an image resource is an enumeration, i.e., it can take a value among its enumeration literals only.

• EnumerationLiteral represents a value that an attribute can have. For example, the status of an image instance can be Failed, Pending or Ready.

Chapter 4. Inferring Precise Models from Cloud APIs Textual Documentations

• RecordType represents a complex DataType to define structures. A RecordType instance appears as a row in the database table. It contains some data about one particular attribute. For example, in GCP, the settings attribute which defines the user settings of a Cloud SQL resource is a record. Each RecordType has at least one RecordField.

• RecordField represents a field of a record. For example, pricingPlan, which is the pricing plan of a resource, and replicationType, which is the replication type of a resource, are record fields of the settings attribute and expect an enumeration type value.

GCP Refinement

Thanks to OCCIware Metamodel, my GCP Model provides a homogeneous specification language for GCP, which tackles the Informal Heterogeneous Documentation drawback, identified in Section 4.2. It also carries out five in-place Model Transformations that propose corrections to face and address the other drawbacks discussed in Section 4.2. They aim for several objectives, especially Type Refinement, Implicit Attribute Metadata Detection, Link Identification, Redundancy Removal and Model Visualization. I highlight in the following these correcting and/or enhancing transformations.

• Type Refinement is done by adopting the data type system proposed by OC-CIware Metamodel, defining regular expressions, and using the EMF validator to check the type constraints that are attached to the attributes. For instance, among the constraints defined for the GCP Model, one constraint states that if the type of an attribute in the documentation is string and the description explains that this is an email address, my GCP Model will apply the email validation constraint for refinement purpose. This kind of information is translated into a StringType containing the following regular expression:

^[A-Z0 -9._%+-]+@[ A-Z0 -9. -]+\\.[A-Z ] { 2 , 6 } $
• Implicit Attribute Metadata Detection to explicitly store information into additional attributes defined in the Attribute concept of my GCP Model. To do so, I apply NLP which has made great progress and has proven to be efficient in acquiring the semantics of sentences in API documentation. Among NLP techniques, I use the Word Tagging/Part-of-Speech (PoS) [START_REF] Klein | [END_REF]] one. It consists in marking up a word in a text as corresponding to a particular part of speech, based on both its definition and its context. For this, I declare my pre-defined tags for some GCP specific attribute properties. Some pre-defined tags are as follows:

-mutable = true if [Input-Only].
mutable = false if [Output-only]/read only.

required = true if [Required].

-required = false if [Optional].
• Link Identification to deduce logical connections between resources. Therefore, I also refer to the idea of applying NLP techniques. This time, I use Syntactic Parsing [Jurafsky 2000] to acquire the semantics of sentences in GCP documentation. The parse tree in Figure 4.14 describes the sequential patterns that allow us to identify the semantics of a link between two resources, namely between an instance and a network in this example. The syntactic parsing is achieved by using Stanford parser [sta], which is a library based on neural network. • Redundancy Removal in order to offer the cloud developers more compact, intuitive and explicit representation of GCP resources and links. To do so, I propose to have some abstractKind instances. An abstractKind is an abstract class from which inherit a group of Kind instances. It allows to factorize their common attributes and actions and to reuse them. This is known as Formal Concept Analysis (FCA) technique [Priss 2006], which is a conceptual clustering technique mainly used for producing abstract concepts and deriving implicit relationships between objects described through a set of attributes.

Chapter 4. Inferring Precise Models from Cloud APIs Textual Documentations

• Model Visualization for an easier analysis of the API, even if the model is not as sophisticated as the original documentation. In fact, when we visualize information, we understand, retain and interpret them better and quicker because the insights become obvious [Moody 2009]. Unfortunately, as discussed in Section 4.2 (lack of visual support), GCP does not currently provide such a visual model. I provide hence, using OCCIware tooling, a model visualization of GCP documentation. I have implemented a prototype of my approach in Java. I used jsoup library3 for building the Snapshot of GCP HTML pages and GCP Crawler, and the Eclipse-based OCCIware Studio for building GCP Model. Readers can find the snapshot of GCP documentation built on July 27, 2017, as well as my precise GCP Model and its code here4 .

Once my model is built, GCP configurations, which represent GCP Instances that conform to GCP Model, can be designed. Then, I aim to elaborate use cases for my model-based GCP configurations as a way of checking them. To do so, I identify the code generation and model interpretation techniques which are two of the advantages of model-driven engineering [START_REF] Schmidt | [END_REF]]. First, with the code generation approach, I aim to use GCP Instances to generate artifacts, such as:

• JSON files that contain the needed structured information for creating a VM for example, through GCP deployment manager,

• CURL scripts that allow us to create a VM for example via the POST action,

• Shell scripts for GCP CLI, and,

• Java or Python code for GCP SDKs to aid in identifying bugs prior to runtime.

Second, I aim to experiment the model interpretation approach, by defining the business logic of GCP Connector. The latter defines the relationship between GCP Instances and their executing environment. For this, the connector provides tools that are not only used to generate the necessary artifacts corresponding to the behavior of GCP actions (create, get, insert, list, patch, update, etc.), but also to efficiently make online updates for the GCP Instances elements according to the changes in the executing environment and to the models@run.time approach [START_REF] Bencomo | [END_REF]]. The generated artifacts will be seamlessly executed in the executing environment thanks to MDE principles [START_REF] Paraiso | Model-driven Management of Docker Containers[END_REF]]. This validation process is entitled "validation by test", because it aims at verifying whether GCP Instances can be executed and updated in the real world. By validating a broad spectrum of GCP Instances, I validate the efficiency of my GCP Model.

Challenges

This contribution of inferring models from APIs might seem simple but it encompasses many challenges like the fact of the documentation is spread over pages. Therefore, one must deeply explore the documentation to completely define all the required elements. For example, when an attribute is an enumeration, we must define the corresponding OCCIware EnumerationType before adding the attribute to the correspondent OCCIware kind. However, as we can see in Figure 4.16, the definition of this enumeration is in another HTML page, and thus the mining of this page is mandatory and preliminary to designing the model. Another challenge of this contribution is the effort and time to toughly analyze the structure of the documentation, which of course contains format inconsistencies making the mining very complicated. This task is necessary in order to design a Documentations correct and resilient crawler. Also, the metadatas are described in natural language in the description, and do not have specific placeholder. So the extraction of this knowledge requires to carefully design the rules that will detect these metadata and put them forward.

Finally, the need to manually check the validity of the extracted model is also a challenge. So far, it is complicated to set up an automatic verification support, and I manually verify the automatically extracted values. For example, if blank spaces were found, I iterate and refine the rules of knowledge extraction.

Evaluation of GCP Model

Thanks to my approach, I perform a qualitative analysis of the GCP documentation and I check if it satisfies three properties: the uniformity, the conciseness and the consistency & comprehensiveness. Then, to evaluate the effectiveness of my model, I report quantitative results that validate the preciseness of my GCP Model.

Qualitative Evaluation

4.4.1.1 Uniformity GCP documentation is not uniform, i.e., it is not written by following the same documentation guideline. In fact, the crawling process has been sophisticated and I ended up implementing two parsing filters to capture the two different formats of the HTML pages (cf. Section 4.2 (heterogeneous documentation format)). For each Kind instance, I noted the filter I used to parse the attributes and the one I used for the actions. This information allows us to reconstruct and understand the map of the GCP development teams. I arrive at the following hypothesis: GCP documentation is developed by two clusters of development teams, as shown in Figure 4.17.

In addition, this classification helps us to predict/learn what teams collaborate together, and to identify the tight links between the GCP development teams and the GCP products. Since the clusters of Kind instances are completely disjoint, I conclude that the two GCP development teams are completely separated.

Conciseness

A cloud API documentation should be concise, i.e., describing all the concepts clearly but briefly and without redundancy. However, this is not the case for GCP documentation. As depicted in Table 4.1, I prove that GCP documentation contains several redundant attributes and actions. Then I show how my approach minimizes the redundancy by introducing the abstractKind concept. Column "Before Abstraction" encompasses the # of occurrences and the % of redundancy for each redundant attribute and action in the official GCP documentation. As for column "After Abstraction", it studies the same aspects but after introducing simply one abstractKind instance in my GCP Model. This instance contains all the attributes and actions of Table 4.1. Columns "Redundant Attributes" and "Re-Chapter 4. Inferring Precise Models from Cloud APIs Textual Documentations dundant Actions" list respectively the names of the attributes and actions that I observed in more than 50% of the resources offered by GCP. For each attribute/action, I show the number of occurrences in columns "# of occurrences", as well as the percentage of redundancy in columns "% of redundancy". Rows "Average" give the average of columns "% of redundancy".

From the results in Table 4.1, I have the following observations. First, I calculate the % of redundancy for all attributes and actions of GCP documentation, which indicates the effectiveness of my approach. Second, these percentages are relatively high, which prove that GCP documentation is redundant. Third, after factorizing the attributes and actions, I succeed to have 66 less occurrences and 46,48% decrease of the redundancy. These results are noticeable and satisfying even with my simple example that consists in only one abstractKind instance included to GCP Model.

Consistency & Comprehensiveness

I have just discussed that some attributes and actions of the GCP resources are redundant. It is not strange to have all these attributes and actions in common. In fact, it makes quite sense that almost each of the Kind instances has an id as an identifier to guarantee that a resource is unique, a kind as this is the type of the resource, a selfLink as a URL that can be used to access the resource again, a description to report and explain the use of this resource, etc. In addition, it is normal that every Kind instance has a list of operations so it can be created, updated, retrieved, deleted, etc.

However, the main problem and what is strange here is why among the 142 resources, the GCP documentation has left 50 without a name or 62 without an id or 63 without a kind or a description, or 2 without delete or 66 without insert, etc. I went further in this research and I checked for each redundant attribute/action the set of Kind instances that are missing it. For example, {compute.beta.regionInstanceGroup, compute.v1.regionInstanceGroup} is the set of Kind instances that does not contain the delete action. In this case, it is comprehensible that the developer has no right to delete, for both compute versions, the regionInstanceGroup concept, which refers to the virtual machines in a particular region.

Another example is regarding dataproc.v1.cluster Kind instance, which describes the identifying information, configuration, and status of a cluster of Google Compute Engine instances. dataproc.v1.cluster belongs to the set of kinds that miss the name attribute and also to the set of kinds that miss the description attribute. In the first set, i.e., the one that misses the name attribute, dataproc.v1.cluster substitutes the name attribute by the clusterName attribute. Although these two have the same semantics, using different vocabulary to express it will lead to nothing but a confusion for the developer. Therefore, I deduce from this example that GCP documentation is inconsistent, i.e., does not employ the same words to define the same characteristics of its services. In the second set, the description attribute is effectively missing and this is not justifiable. I can then state that GCP documentation is not comprehensive, i.e., it contains some oversights or incompleteness.

Quantitative Evaluation

To evaluate the preciseness of my model, I conduct using my GCP Crawler an automated and recursive analysis of the GCP official documentation. First, I perform a global investigation to identify, quantify and sort the provided services. This analysis allows us to declare that GCP API contains 142 resources packaged into 14 products as listed in Table 4.2. Each product offers a service like Big Data, Compute, Network, Management, Storage & Databases, etc. Besides the 142 types of resources, GCP documentation contains 2124 attributes that describe the static aspect of the API, and 985 actions that describe its dynamic aspect. In addition to these precise statistics that I provide, my approach allows to clearly specify GCP attributes thanks to the Type Refinement and the Implicit Attribute Metadata Detection. Also, unlike GCP official documentation, my model uses a DataType validator at design time to validate the types defined before the provisioning. This validation guarantees the coherence and preciseness of the GCP configurations that must be conform to GCP Model, which is an efficient abstraction of the GCP API.

Summary

In this chapter, I proposed the first approach that analyses cloud API documentations and applies NLP techniques to extract model-driven specifications. A major use case was carried out on GCP. I highlighted six main drawbacks of GCP documentation and I argued for the need of inferring a formal specification from the current natural language documentation. To address the problem of informal heterogeneous documentation, I present my model-driven approach which consists in a GCP Model that conforms to the OCCIware Metamodel presented in Chapter 3. Using my GCP Crawler, my model is automatically populated by the GCP resources that are documented in plain HTML pages. I also proposed five Model Transformations to correct the remaining five drawbacks. Finally, my approach allowed us to deduce some facts regarding the uniformity, conciseness, consistency and comprehensiveness of GCP API. To conclude, I validated the preciseness of my model by providing quantitative results on GCP API.

In the next chapter of this dissertation, I present my approach for reasoning on cloud APIs in order to verify their behaviour and understand their similarities.

Chapter 5

Specifying Heterogeneous Cloud

Resources and Reasoning over them with fclouds

This chapter is a combined and extended version of our papers "Specifying Semantic Interoperability between Heterogeneous Cloud Resources with the FCLOUDS Formal Language" [Challita 2018b] published in the 11th IEEE International Conference on Cloud Computing (CLOUD) and "Towards Formal-Based Semantic Interoperability in Multi-Clouds: The FCLOUDS Framework" [Challita 2017b] published in the 10th IEEE International Conference on Cloud Computing (CLOUD). C hapter 2 reviewed the solutions for multi-cloud interoperability. To be effec- tive, these solutions must achieve a compromise between defining the common cloud principles and supporting any kind of cloud resources, regardless of their abstraction level. This frustrating situation calls for more depth about the cloud providers' semantics to reason about the common principles that interoperability solutions must adhere to.

In this chapter, I present my vision for reasoning on cloud solutions via fclouds, my framework for semantic interoperability in a multi-cloud context. By semantic interoperability I mean to identify the similarities and differences between cloud APIs concepts and to reason over them. My framework contains a catalog of cloud APIs that are precisely described. It will help the cloud customer to understand how to migrate from one API to another, thus to promote semantic interoperability. To implement the formal language that will encode all the APIs of my fclouds framework, I advocate the use of formal methods, i.e., techniques based on mathematical notations. They will allow me to rigorously encode cloud concepts and behaviour, validate desired and/or imposed cloud properties and finally define formal transformation rules between cloud concepts. For more reliability, I adopt the concepts of the OCCI common standard to define the formal language of the fclouds framework. I choose to formalize OCCI with Alloy, a lightweight promising formal specification language designed by Daniel Jackson from the MIT [Jackson 2012].

The key contributions of this chapter are:

1. the fclouds framework, my formal approach for semantic interoperability in multi-clouds, 2. the fclouds language, the formal language of the fclouds framework, which consists in a formalization of OCCI concepts and operational semantics in Alloy, 3. the identification of five properties (consistency, sequentiality, reversibility, idempotence and safety) that reflect OCCI RESTful operational semantics, and their validation in fclouds, which ensures the language correctness, 4. a catalog of thirteen formal specifications of cloud APIs from different application domains, encoded with fclouds language, which prove the language expressiveness, and, 5.1. Exploring the Semantic Space 123 5. formal transformation rules between heterogeneous concepts with similar semantics.

This chapter is structured as follows. Section 5.1 outlines the need to reason on the "Cloudware engineering" solutions, explains the motivations behind exploring their semantics and positions my contribution in relation to the related works. Section 5.2 presents my framework fclouds, its components and a usage scenario. Section 5.3 presents the fclouds language that specifies OCCI core concepts and operational semantics, and verifies properties on how OCCI should work. Section 5.4 illustrates the use of my formal language with a series of thirteen examples. Finally, I conclude in Section 5.5.

Exploring the Semantic Space

A set of common principles that all interoperability solutions adhere to must be agreed on. Accordingly, I argue in the following for the need to explore the Semantic space. The latter will allow the cloud architect to rise in abstraction and reason about cloud APIs through the use of formal methods, as shown in Figure 5.1.

Formal methods and their benefits

Formal methods are techniques that are based on mathematical notations and they will allow me to rigorously encode the underlying semantics of cloud APIs concepts through formal specifications. Formal specifications remove ambiguities, since unlike natural language statements, mathematical specifications are only interpreted in one way, the correct one. This focuses on what a system should do rather than how to accomplish it. Formal methods also allow me to effectively reason on the structure and behaviour of the encoded concepts, by using a model checker verifying cloud over them with fclouds properties, i.e., constraints denoting characteristics of cloud configurations and/or operations. This is quite advantageous to guarantee the accuracy and correctness of the multi-cloud solutions, and because the earlier a defect is removed the cheaper it will be to correct it. Being precisely specified, verified and correctly understood, the cloud APIs can be correctly compared. For this, I will define formal transformation rules between their concepts, and verify equivalence properties. The developers will hence be able to achieve semantic interoperability in a multi-cloud system.

For the above reasons, I propose in the current work to rise in abstraction by heading towards using formal models and verification for cloud computing.

Related Work

Only few works from the literature applied formal methods for the cloud, which proves the novelty of this domain. [START_REF] Benzadri | [END_REF]] proposed a formal model for cloud computing using Bigraphical Reactive Systems (BRS). AWS [START_REF] Newcombe | [END_REF]] used TLA+ specification language in their complex systems such as S3 and DynamoDB. Bobba et al. [Bobba 2017] specified and validated Google's Megastore, Apache Cassandra, Apache ZooKeeper, and RAMP using Maude language and model checker. Besides using different techniques to reason over the cloud, these three works differ in their objectives too. [START_REF] Benzadri | [END_REF]] reasons over cloud concepts for deployment and adaptation purpose. [START_REF] Newcombe | [END_REF]] aims at finding subtle bugs in their internal distributed algorithms, which helps correcting and optimizing their systems. [Bobba 2017] verifies the performance and correctness of cloud storage systems. My work focuses on the interoperability concern by formalizing the static and operational semantics of the cloud domain.

From the literature, I found out that semantic interoperability between cloud domains has been also achieved with techniques different from formal methods. For example, the authors in [Yongsiriwit 2016] proposed an ontology-based framework for semantic interoperability in multi-clouds. They define translations between IaaS concepts of three standards. However, they do not consider any mapping between API operations. Also, PaaS Semantic Interoperability Framework (PSIF) [START_REF] Loutas | [END_REF]], which was implemented in the context of Cloud4SOA project, proposes common PaaS models that describe structural, functional and behavioural semantics. fclouds goes beyond PSIF and aims to verify properties of the models thanks to the usage of formal methods. I assume that a developer would like to build a multi-cloud system spread over two clouds, the private EGI FC and the public GCP. EGI is based on OCCI REST API and GCP on its own REST API, so the developer is faced to two heterogeneous APIs implementing different concepts and paradigms. To provision a virtual machine, the HTTP request has a different format for each API, which is quite frustrating. The developer would like a single API for both clouds to seamlessly access their resources. However, the GCP API will not work on OCCI and if OCCI wanted to provide equivalent services to GCP, it should not only adopt the same type of API but also the same concepts with the risk of misunderstandings, inconsistencies and incompleteness. Conflicts and misunderstandings about the semantics over them with fclouds of cloud providers can be solved, or at least identified at an earlier stage, if aspects of structure and operations are conveyed through the use of formal models.

As depicted in Figure 5.2, the first stage of fclouds requires extracting from websites, in a manual or automated way, knowledge regarding the services offered by cloud providers. Then, I proceed by a precise modeling to understand and validate the behaviour of cloud APIs, in order to overcome their semantic heterogeneity. In the second stage of fclouds, I proceed with transformation models, which explain how knowledge collected against one cloud provider can be transformed to fit another. This stage allows a rigorous comparison and semantic connections between cloud providers.

Overall Architecture

fclouds framework is based on several cloud formal models that can be composable. It consists of a formal model for OCCI (fOCCI), a formal model for GCP (fGCP), a formal model for Docker (fDocker), etc. (see the rectangles in Figure 5.3). Later on, I will define transformation rules that find equivalence and specialization relationships between them, thus I can seamlessly achieve semantic interoperability (see the ovals in Figure 5.3). The green shapes represent some of the APIs and the transformation rules that are specified in my fclouds framework (see Section 5.4 for the entirety of fclouds APIs) and the orange shapes represent an API and transformation rules that are considered for future work. In the following, I detail the process of formalizing cloud APIs, which is at the basis of fclouds framework. As shown in Figure 5.4, it is developed in two main steps: Modeling and Reasoning.

Modeling

Modeling using formal methods is the process of providing a precise specification of a cloud model, i.e., defining and validating:

• Cloud structure and constraints, as represented in Frame (1) in Figure 5.4, to denote the types of cloud concepts such as virtual machines, containers, storage, operating systems, servers, applications, etc. and describe configurations of these types. fclouds models support cloud computing concepts specification while simplifying irrelevant details to focus on the most important characteristics.

• Cloud API operations, as represented in Frame (2) in In my work, I choose the Alloy formal language to provide a concise specification of fclouds models, with both a graphical output and a textual output, so it can be easy to analyze and reason over them. More details about this language, called the fclouds language are given in Subsections 5.3.2 and 5.3.3. over them with fclouds

Reasoning

Using formal models has the advantage of allowing reasoning over concepts and operations for a better understanding of their semantics and how they work. Therefore, once fclouds models have been specified, I proceed by the definition and verification of cloud structural and behavioural properties as shown in Frame (3) in Figure 5.4. This step allows to ensure the correctness of all cloud formal models in the fclouds framework, so I can draw later inferences between them. More details about cloud properties are given in Subsection 5.3.4.

The fclouds Language

The formal language on which is based the fclouds framework and that I propose, is called the fclouds language. It is an Alloy-based formal language which makes explicit OCCI core concepts [Nyrén 2016b] and OCCI REST operations [Nyrén 2016a], as well as the underlying properties.

Notations

I argue it is more advantageous and reliable to adopt an open standard to define the formal specification language of all fclouds APIs, instead of writing a language from scratch. The most popular standard is OCCI since it is used by the private EGI FC and it was successfully extended to support heterogeneous aspects of the cloud domain, through OCCI Infrastructure [Nyrén 2016c], OCCI Platform [START_REF] Metsch | [END_REF]], etc. In fact, OCCI defines a generic and extensible model for cloud resources and a RESTful API for efficiently accessing and managing resources. This facilitates interoperability between clouds that are implemented as OCCI extensions, i.e., specified by the same OCCI resource model, and accessed by the same REST API. Today, there are several trends for formal methods like Petri nets, languages based on logic, semantics programs, automata theory, etc. Choosing the appropriate notation is critical in order to find the right compromise between formalization and complexity. Meanwhile, Alloy is becoming increasingly popular among formal methods, as it is a relational, first-order logic language, with well-thought out syntax and model visualization features. Alloy is a lightweight promising formal specification language designed by Daniel Jackson from the MIT [Jackson 2012]. It allows to specify complex systems in a streamlined way, by describing concepts and constraints. The specifications are translated into first-order logic expressions that can be automatically solved by the Alloy analyzer, a model checker using SATisfiability (SAT) solvers. The latter allows automatic verification of a system model, to ensure its consistency and other desired properties, thus to guarantee its correctness. Therefore, I choose to formalize OCCI using a lightweight promising formal language, the Alloy specification language [Jackson 2012]. I refer to this formal specification as the fclouds language.

In the following, I present a subset of the fclouds static and operational semantics. For more details, the entirety of this language is available in the OCCIware official website [Ahmed-Nacer 2016b] and in this GitHub repository1 .

Specifying fclouds Static Semantics

The static semantics of fclouds corresponds to the formalization of the OCCI core concepts [Nyrén 2016b] in Alloy. I use a strategy based on Time dimension [Jackson 2012]. It allows to distinguish between mutable fields, i.e., those that are related to Time, and immutable ones, i.e., those that are not related to Time. I detail in the following the twelve concepts of fclouds in Alloy:

• Entity represents an abstract type defining the set of all resources and links. a b s t r a c t s i g E n t i t y { i d : one S t r i n g , kind : one Kind , m i x i n s : s e t Mixin -> Time , a t t r i b u t e s : s e t A t t r i b u t e S t a t e -> Time }

A signature (sig) in Alloy defines a set of atoms. An atom is an indivisible, immutable and uninterpreted unity. Signature declarations can introduce fields. A field represents a relation among signatures. For example, Entity declares four fields: id, kind, mixins and attributes. Each entity instance has a unique identifier (id). A declaration of the form id : one String can be read as declaring a feature of the set Entity; formally, it declares a binary relation between the set of entities, Entity, and the set of Strings, String. The one multiplicity keyword signifies that the relation between a tuple from id and a tuple from String has a 1..1 cardinality. The kind field is the Entity type, for example the kind of a resource can be Compute, Application, etc. The mixins field is used to add additional features such as location and price. The set multiplicity keyword signifies that mixins can contain any number of elements. The id and kind are immutable. As for the mixins and attributes 130 Chapter 5. Specifying Heterogeneous Cloud Resources and Reasoning over them with fclouds fields, they are mutable and they identify the association between Mixin atoms and their Time, and the association between AttributeState atoms and their Time . mixins and attributes are ternary relations. mixins relation associates entities, mixins and times, whereas attributes relation associates entities, attributes and times.

• Kind is the Entity type. For example, the kind of a resource can be Compute, Network, Application, etc. The extends keyword in Alloy indicates that a set is declared as a subset of another one and that it will form, with other subsets similarly declared, a partition of the set it extends. A Kind instance can have zero or one parent kind. The lone keyword is an example of a relation multiplicity. In our case, it signifies that a given Kind is to be associated to at most one parent. A Kind instance can also have zero or many actions and zero or many entities. The parent and actions fields are immutable. Only the entities field is mutable because entities (resources or links) can be created/added or deleted/removed at runtime. The entities associated to a certain kind cannot have the same id. This is defined through the following constraint, which must always hold, i.e., an invariant. a l l t : Time | no d i s j e1 , e2 : e n t i t i e s . t | e1 . i d = e2 . i d This invariant takes the form of a basic first-order logical formula, and it says that for every time, there is no pair of distinct entities that have the same id. The all keyword denotes the universal quantifier, where a declaration such as t : Time denotes an arbitrary element t of the set Time. The no disj keyword means that kinds do not have overlapping entities. Likewise, the dot notation e1.id or e2.id is the standard notation for accessing a feature, or attribute, of an instance of a signature. In this case, the dot serves to access the id feature of an entity instance.

• AttributeState represents an instantiated OCCI Attribute. s i g A t t r i b u t e S t a t e { name : one S t r i n g , v a l u e : one S t r i n g } An AttributeState instance has exactly one name and one value.

• Attribute is the property of an entity like machine hostname, IP address of a network, parameter of an action, etc. An Attribute instance has exactly one name and can have zero or one information whether it is mutable or not, required or not and has multiple values or not. However, Boolean type is not supported by Alloy for declarations. Therefore, in order to express these fields, I use util/boolean library that defines a boolean type sig Boolean { } with one sig True, False extends Boolean { }. An Attribute instance can also have zero or one default value and zero or one description. All the attributes fields are immutable.

• DataType is the abstract class used to extend the non-extensible data type system of the OCCI specification. Since attributes can have scalar data types (IP address, float, etc.) and enumeration, the classical data types defined as strings, booleans and integers are insufficient and require to be extended.

a b s t r a c t s i g DataType { name: one S t r i n g } A Datatype instance has exactly one immutable name such as array, enumeration, record, etc.

• Mixin is a concept that adds additional features to OCCI entities. A Mixin instance can contain zero or many actions, it can depend from zero or many of mixins, i.e., if Mixin A depends from Mixin B, any entity associated to Mixin B will inherit the capabilities (attributes and actions) of both Mixin B and Mixin A. Mixin can be also applied to zero or many kinds, i.e., add new capabilities to the kind instances. A Mixin instance has zero or many entities that are associated to it. Only the entities field is mutable. A Mixin instance must not inherit/depend from itself directly or transitively. This constraint is ensured as follows:

no d : t h i s . ^@depends | d = t h i s
This constraint specifies that the relation between mixins is acyclic, i.e., the relation between mixins do not form a ring. It denotes that there is no mixin that belongs to the set of targets reachable from the same mixin itself. The no quantifier means that this constraint is true when for d = this is true, there is no bindings of the d variable. In other words, d does not have a value if it belongs to the this.ˆ@depends relation and is equal to the mixin instance itself. The "ˆ" operator denotes the transitive closure of the depends relation, i.e., the smallest enclosing relation that is transitive. The "@" symbol is used to prevent the depends field from being expanded. Without the @ symbol, the constraint would instead be short for:

no d : t h i s . ^( t h i s . depends ) | d = t h i s
which does not even type-check.

• Action represents an operation that can be executed on an entity instance such as start virtual machine, stop virtual machine, restart an application, resize a storage, etc.

s i g Action e x t e n d s Category { }

• Category is the abstract class of all the Action, Kind and Mixin instances.

a b s t r a c t s i g Category { term : one S t r i n g , scheme : one S t r i n g , t i t l e : l o n e S t r i n g , a t t r i b u t e s : s e t A t t r i b u t e }

A Category instance has exactly one term, one scheme and may have or not one title. A Category instance also contains a set of attributes. The attribute name must be unique, as defined by the following constraint: no d i s j a1 , a2 : a t t r i b u t e s | a1 . name = a2 . name This constraint means that there is no pair of distinct attributes that have the same name. All the Category fields are immutable.

• Resource represents a concrete cloud computing resource, which refers to any entity hosted in a cloud, e.g., compute1 is a resource that belongs to Compute kind, network3 is a resource that belongs to Network kind, storage2 is a resource that belongs to Storage kind, etc. Link contains two mutable fields: source and target. Each sourced link must have a target, as defined by the following constraint: over them with fclouds one s o u r c e i m p l i e s one t a r g e t

The one quantifier applied before the "source" expression means that the set of sources has exactly one tuple, i.e., for a Link l, l.source is the resource that l is currently sourced to. Similarly, the one quantifier applied before the "target" expression means that the set of targets has exactly one tuple, i.e., for a Link l, l.target is the resource that l currently targets. This constraint means that the one source constraint implies the one target constraint.

• Extension is a set of kind and mixin instances targeting a concrete cloud domain (IaaS, PaaS, SaaS, pricing, SLA, cloud monitoring, etc.). An Extension instance has one name and one scheme. It can use or extend zero or many extensions. It owns zero or many kinds, mixins and datatypes. All the Extension fields are immutable. The scheme of all kinds must be equal to the scheme of the owning Extension instance, as defined by the following constraint:

a l l k : k i n d s | k . @scheme = scheme
This constraint means that for every kind of an extension, the scheme of this kind is equal to the scheme of the extension.

• Configuration is the abstraction of an OCCI-based running system. Modeling a configuration offline allows designers to think and analyze their cloud systems without having to deploy them concretely in the clouds [Merle 2015a]. The use field, which is the set of extensions used in a configuration, is immutable because the extensions cannot be added or removed at runtime. The resources and mixins fields are mutable. The kind of all resources of a configuration instance must be defined by an extension that is explicitly used by this configuration. This constraint can be expressed as follows: This constraint means that for every time, the extensions containing the kinds of the configuration resources are contained in the extensions of this configuration. In Alloy, the in keyword denotes the subset relation.

Specifying fclouds Operational Semantics

The operational semantics of fclouds corresponds to the formalization of the informal OCCI behavioural specification detailed in [Nyrén 2016a]. It mainly includes different REST operations, i.e., CREATE, RETRIEVE, UPDATE, DELETE. In this idiom, these operations are modeled as predicates that specify the relationship between pre-state, i.e., the state before the operation is called and post-state, i.e., the state after the operation is completed. To do so, Time is added at the end of each mutable field to represent the state concept. To be more specific, an operation op will be specified using a predicate: pred op[...,t,t':Time] ..., over them with fclouds with two special parameters t and t' denoting, respectively, the pre-and poststates [Garis 2012]. The core of each predicate is carried out by defining explicitly pre-and post-conditions, which are constraints that must be satisfied before executing the operation and after the operation is finished respectively. Eight operations were defined to the Configuration concept of fclouds, as depicted in Table 5.2. I present in the following the four REST operations applied to resources.

Create semantics

The following predicate shows how I formally specify the creation of a resource. At time t, I specify that a configuration, passed as argument to the predicate, does not have a resource with the id passed as a predicate argument (cf. line 3). The no quantification keyword expresses the null cardinality of the empty resource set that satisfies the constraint resource.id = resourceId. As well, I specify that the kind and the mixins of the resource I want to create, are contained in the configuration extensions (cf. lines 4 and 5). At time t', I add to the configuration resources, one resource with the id, kind, mixins and attributes, passed as argument to the predicate (cf. lines 7 to 12). The "+" operator denotes set union. I also explicitly specify that the mixins of the configuration remain unchanged (cf. line 14).

Retrieve semantics

The following predicate shows how I formally specify the retrieval of a resource. At time t, I verify that a configuration has one resource with the id passed as a predicate argument (cf. lines 4 and 5). At time t', I specify that the id, mixins, attributes and links of the retrieved resource remain unchanged (cf. lines 8 to 12). I also specify that the resources and the mixins of the configuration remain unchanged (cf. lines 14 and 15).

Update semantics

The following predicate shows how I formally specify the update of a resource.

pred UpdateResource [ c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , a t t r i b u t e 1 : A t t r i b u t e S t a t e , a t t r i b u t e 2 : A t t r i b u t e S t a t e , t , At time t, I specify that a configuration, passed as argument to the predicate, has a resource with the id passed as a predicate argument and with the attribute, attribute1 which is also passed as a predicate argument (cf. line 4). The "&&" operator denotes conjunction of constraints. I also specify that the attribute1, passed as argument to the predicate, is different from attribute2, also passed as argument to the predicate (cf. line 5). The "!=" operator is the negation operator "!" associated to the comparison operator "=" and is equivalent to not attribute1 = attribute2. At time t', I update the existing attribute state of my resource, i.e., attribute1, with the value of the new attribute state, i.e., attribute2 (cf. lines 7 and 8). The "++" operator is used for the override, which means that the tuples of attribute2 replace the tuples of attribute1. I also explicitly specify that the resources and the mixins of the configuration remain unchanged. Only the attributes of one resource change (cf. lines 10 and 11).

Delete semantics

The following predicate shows how I formally specify the deletion of a resource. At time t, I specify that a configuration, passed as argument to the predicate, has a resource with the id passed as an argument (cf. line 3). At time t', I remove from the configuration resources, one resource with the id passed as argument to the predicate (cf. lines 5 to 7). The "-" operator denotes set difference. I explicitly specify that the mixins of the configuration remain unchanged (cf. line 9).

Identifying & Validating fclouds Properties

Using formal languages has the advantage of allowing reasoning over concepts and operational semantics for a better understanding of their semantics and how they work. Therefore, once the fclouds formal language has been specified, I proceed by the definition of some structural and behavioural properties to ensure its correctness and to express its desired/required behaviour. I formally encode the consistency, sequentiality, reversibility, idempotence and safety behavioural properties. The last two properties are classified into a broader property which is the conformance to HTTP 2 protocol [START_REF] Belshe | [END_REF]]. Then, using the Alloy analyzer, I validate that these properties adequately hold in my fclouds static and operational semantics. To express these properties, assertions are written and are expected to hold as consequence of the specified constraints. In order to be confident that an assertion holds, I check it within a reasonable scope, i.e., I bound the number of atoms allowed for each signature to 10. If no counterexamples are returned by the Alloy analyzer with such a scope, I can be confident that my language reflects the desired semantics.

Consistency

fclouds language is consistent if it does not contain any contradictory constraints, so its concepts can be instantiated and each cloud API operation can be executable. I can also analyze what could not be instantiated, thus can't be deployed in realworld. In these cases, my formal language might be over-constraining so I deem necessary to relax some constraints. The CreateResourceIsConsistent assertion below can't be shown to have a counterexample. Hence, it asserts the existence of a valid configuration that meets the pre-and post-conditions of Create Resource, i.e., it is consistent and expresses the desired behaviour.

Sequentiality

Two cloud API operations are sequential when one cannot happen if the other one did not happen at the time before. For example, the developer can adapt the performance of a virtual machine only if it was created before.

It is explicitly stated in the informal specification of OCCI that Update Resource operation should be preceded by Retrieve Resource operation: "Before updating a resource instance it is RECOMMENDED that the client first retrieves the resource instance" [Nyrén 2016a]. I also explicitly specify in fclouds that Retrieve Resource operation must be preceded by Create Resource operation (as shown in the following assertion), Update Link by Retrieve Link and Retrieve Link by Create Link.

Conformance to HTTP 2 Protocol

As OCCI is a REST architecture that conforms to the HTTP protocol, it must conform to its specification too. Therefore, there are some imposed properties I must have in any REST-based systems so they must be checked in the fclouds over them with fclouds language. According to the Request For Comments (RFC) HTTP 2 [START_REF] Belshe | [END_REF]], I identified two properties of the HTTP methods and I verified in my formal language that the appropriate pairs of operations respect these properties.

1. Idempotence: a method is idempotent when it always produces the same server external state even if applied several times [START_REF] Belshe | [END_REF]]. In HTTP, GET, PUT and DELETE methods are idempotent. In OCCI, Retrieve operation is associated with a GET HTTP method, Create operation is a PUT HTTP method and Delete operation is a DELETE HTTP method. So I verify in my formal language that Retrieve Resource, Retrieve Link, Create Resource, Create Link, Delete Resource and Delete Link are idempotent. For example, as a result, the following assertion is valid: This assertion checks if creating a resource induces the same configuration at times t.next and t.next.next. In contrast, an Update operation, referred to as a POST in HTTP, is not idempotent. Therefore, the accuracy of my fclouds language is maintained if the following assertion is not valid: 2. Safety: a method is safe when it does not change the external server state [START_REF] Belshe | [END_REF]]. It mainly concerns the retrieval of information. A safe method is necessarily an idempotent method, but not the reverse way. In HTTP, a GET method is safe. Therefore, in fclouds, I check that Retrieve Resource and Retrieve Link respect this property, so they do not change the cloud configuration. An example of a safe operation is detailed below: This assertion checks if a configuration remains the same at time t, i.e., before retrieving the resource, and at time t.next, i.e., after retrieving the resource. Table 5.2 lists all the operations that I have modeled, as well as all the properties that have been checked. The "+" symbol represents the operations or the pairs of operations that should fulfill a property, while the "-" represents the operations or the pairs of operations that they should not fulfill this property. By using the Alloy analyzer, I check that the fclouds language, the core language of my fclouds framework, correctly reflects these properties, so I guarantee that it is valid and that I implemented the desired behaviour.

Evaluation of fclouds

To validate the effectiveness of my formal language, I demonstrate how it can be easily adapted to different concerns by providing formal specifications in Alloy for OCCI extensions from different cloud application domains. Therefore, I have surveyed the literature to find all the already published OCCI extensions. I have identified thirteen works that belong to IaaS, PaaS and Internet of Things (IoT) domains, as well as to transverse cloud concerns. As a working hypothesis, I have assumed that all these extensions are correct as they were already accepted through a peer review process. My validation allows me to confirm:

1. the power of expression of my fclouds language (Subsection 5.4.1), 2. the validity of the fclouds behaviour I defined, on all of the OCCI extensions (Subsection 5.4.3), 3. the ability of my language to define domain-specific properties (Subsection 5.4.4), and, over them with fclouds 4. its ability to encode equivalence predicates, i.e., transformation rules between heterogeneous concepts, and to define properties of the equivalence (Subsection 5.4.5).

Catalog of Cloud Formal Specifications

Thanks to my proposed formal language, I succeeded to precisely encode thirteen heterogeneous APIs, as shown in Table 5.3 that gives a summary of my fclouds framework dataset. For each concept of my language, Table 5.3 provides the number (#) of instances of this concept present in the dataset. The last line provides the total of fclouds concepts present in the dataset. For brevity, I give in the following excerpts of the formal APIs' specifications, implemented beforehand as OCCI extensions. Full specifications for each of these thirteen extensions can be found in the supplemental material here 8. OMCRI [Merle 2017] is an application of OCCI for Robot-as-a-Service domain.

The OMCRI extension defines generic and specific robot resource types.

9.

CoT is an application of OCCI for seamlessly provisioning cloud and IoT resources [START_REF] Rachkidi | [END_REF]].

10. OCCI SLA [Katsaros 2016] defines OCCI types for modeling service level agreements.

11. OCCI Monitoring [START_REF] Ciuffoletti | Open Cloud Computing Interface -Monitoring Extension[END_REF]] is a draft specification of OCCI that defines sensor and collector types for monitoring cloud systems.

12. Cloud Simulation [Ahmed-Nacer 2016a, Ahmed-Nacer 2017] is an application of OCCI to simulate cloud systems. The Cloud Simulation extension defines two notions: (i) a resource to simulate that represents the resource to be simulated, and (ii) a simulation resource that represents the resource which performs the simulation activity.

13. Cloud Elasticity [Zalila 2017b] is an application of OCCI that defines a controller resource type to provide strategies for automatically provisioning and de-provisioning compute resources such as memory and cores.

Implementation of fclouds Formal Specifications

To provide the formal specifications of OCCI extensions, I implemented Alloy Generator, which is an Acceleo [acc] generation module added to the OCCIware tool chain. Acceleo is a model-to-text generator, i.e., as illustrated in Figure 5.5, it takes an OCCI extension and generates a text file, which an Alloy specification in our case. This specification conforms to the fclouds specification. Acceleo uses a template-based approach. This approach mixes static parts, which are raw text that will be outputted as it is, and templates, which are text that contains special part which will be filled with information from the model. Let's consider the example in Figure 5.6, which represents the template that is responsible of generating an Alloy signature for each kind of an OCCI extension. "one sig" and "extends Kind" are static parts, whereas the values between brackets will be replaced by values of the extension kinds (cf. line 1). In this template, we can see that there are conditionals on concepts (cf. lines 3, 5 and 7). For instance, if there is no actions, then we print "no actions". Otherwise, for each action, we use a dedicated template (cf. line 7). In fact, in our Alloy Generator, I created templates for each OCCI concept to create the corresponding Alloy concept.

Transformation Rules for Semantic Interoperability in Multiclouds

The last step for achieving semantic interoperability between heterogeneous domains is to define predicates that implement bidirectional formal transformation rules to map between resources with similar semantics. In the following example, I show how I can migrate from an OCCI Infrastructure virtual machine at to a GCP virtual machine. I map the attributes of a given Compute resource to those of an Instance resource. Also, since I learned from the OCCI Infrastructure and GCP documentations that the memory in OCCI is expressed in gigabytes, whereas it is in megabytes in GCP, I applied the multiplication operator for the conversion.

pred ComputeMapInstance [ c : one Compute , i : one I n s t a n c e ] { i . machinetype . guestCpus = c . occi_compute_cores i . name = c . occi_compute_hostname i . machinetype . isSharedCpu = c . occi_compute_share i . machinetype . memoryMb = mul [ 1 0 2 4 , c . occi_compute_memory ] i . s t a t u s = c . occi_compute_state i . s t a t u s M e s s a g e = c . occi_compute_state_message } Such formal equivalence rules and properties are capable of gaining huge time and development costs. The cloud developer can now verify a priori the feasibility of his/her multi-cloud system, before embarking on error-prone implementations. Thanks to my transformation rules and to MDE principles, I can later imagine a model that factorizes common attributes for re-usability between OCCI Infrastructure and GCP.

Summary

This chapter presented the fclouds framework, my approach that relies on formal specification techniques, specifically on the Alloy language, to rigorously and clearly describe the requirements of cloud APIs. I formalize the OCCI standard in order to implement my formal language for the clouds. My formal specification of OCCI was checked for validity thanks to the Alloy analyzer that provides a verification backbone for OCCI properties. To demonstrate the usefulness of my approach, I conducted thirteen case studies to show how my approach is applied on OCCI extensions and that these thirteen APIs with different functionality verify the OCCI properties so they correctly comply to the OCCI standard. Also, applying Alloy to these APIs allowed me to reflect the proper behavior of each API by identifying and validating its specific properties. Finally, having rigorously specified the static and operational semantics of each cloud API, I defined formal transformation rules between their formal specifications, thus ensure semantic interoperability between them.

This chapter concludes the fourth part of this dissertation, i.e., the contributions. In Chapter 4 I described how I automatically extracted a precise model from GCP documentation to provide an accurate description of GCP API. Afterwards, Chapter 5 described how I formally verified that cloud APIs reflect the desired behaviour and how I achieved semantic interoperability between their concepts with the fclouds framework.

In the following part, I summarize the main contributions of this thesis, present the conclusions of the research work, and define a set of perspectives for future work.

Chapter 6 This last chapter summarizes the contributions of this thesis and discusses future research lines of the work presented in this dissertation. It is structured as follows. Section 6.1 recapitulates the OCCIware research project that supports this thesis. In Section 6.2, I summarize the contributions of this thesis. Section 6.3 states shortterm and long-term perspectives to extend this research. Section 6.4 concludes this manuscript.

Conclusions and Perspectives

Background Summary

This thesis is supported by the French OCCIware project and promotes its advancement. OCCIware addresses:

• RQ#1: Is it possible to have a solution that allows to represent all kinds of cloud resources despite their heterogeneity, and a complete framework for managing them?

OCCIware platform is summarized as follows:

A complete modeling, verification, generation and management support. MDE approaches have proven to be advantageous to address the heterogeneity across cloud providers. However, the existing MDE approaches for the cloud, are limited to designing cloud infrastructures. Cloud developers need support to deploy and manage, not only design all the kinds of cloud resources. Automating the deployment of cloud artifacts and managing different types of cloud resources at runtime are not straightforward. To tackle these issues, I introduced the OCCIware approach in Chapter 3. This solution is based on well accepted and defined standards and technologies. In particular, OCCIware relies on the OCCI standard that proposes a generic model and API for managing any kind of cloud computing resources. Also, OCCIware exploits the principles of MDE and leverage them to provide modeling, verification, generation and management support for cloud extensions and configurations. The OCCIware approach especially provides the OCCIware Metamodel, which is based on an Ecore syntax and allows to define cloud concepts with OCL constraints over them. The OCCIware Metamodel can be seen as a domain-specific modeling language to define and exchange OCCI extensions and configurations between end-users and resource providers. For tooling purpose, the OCCIware Studio is a tool chain built on top of the OCCIware Metamodel. The OCCIware Studio allows both cloud architects and users can encode OCCI extensions and configurations, respectively, graphically via the OC-CIware Designer tool, and textually via the OCCIware Editor tool. They can also automatically verify the consistency of these extensions and configurations via the OCCIware Validator tool, generate dedicated model-driven tooling via both Ecore Generator and Connector Generator tools, generate a deployment script via the CURL Generator tool, and manage their configurations at runtime via the generated connectors deployed in OCCIware Runtime.

Contributions Summary

The two contributions of this thesis are made as part of my work around the OC-CIware platform. The first contribution addresses:

• RQ#2: Is it possible to automatically extract precise models from cloud APIs and to synchronize them with the cloud evolution?

The second contribution addresses:

• RQ#3: Is it possible to reason on cloud APIs and identify their similarities and differences?

The two contributions are respectively summarized as follows:

An automated knowledge extraction support. As cloud environments evolve over time, their models have to evolve as well to be kept up-to-date. However, nearly all the existing models that represent the cloud environment are manually 6.2. Contributions Summary 155 built, which is tedious and error-prone. In addition, the defined vocabulary of the existing cloud models is not rich enough to cover the heterogeneity of all existing resources. It only considers the lowest common denominator of the cloud providers. It should also be noted that the defined vocabulary is not flexible enough and there is no information provided on how the developer can extend this vocabulary. In Chapter 4, I thus introduce my approach of inferring precise models from cloud textual documentations. To experiment this approach, I studied the documentation of GCP that presents various drawbacks. Later on, I implemented a crawler that automatically extracts GCP resource types, their attributes and operations. These resources are stored in GCP Model that conforms to the OCCIware Metamodel and is built as an OCCI extension using the OCCIware Studio. I showed that using MDE to specify GCP API improve the specification of GCP, especially via the model transformations like refining the types of the attributes and detecting implicit metadata. A precise specification, accompanied by a validator at design time, helps the developer to ensure correctness of his/her GCP configurations before their deployment. I also showed that using such a model-driven specification leads to a redundancy reduction, even with a simple transformation, i.e., by introducing a single abstract kind to the specification. My approach also allowed me to deduce some facts regarding the uniformity, conciseness, consistency and comprehensiveness of GCP API.

A formal specification support. Cloud solutions (APIs, services, standards and model-driven approaches) are numerous and heterogeneous. Moreover, there is no clear consensus on how these solutions work. And although MDE approaches allow the developer to validate cloud configurations before their deployment through OCL constraints, the developer needs to logically think and understand the cloud solutions. Developers need a formal specification of cloud solutions, fclouds is the first approach ensuring this support. As explained in Chapter 5, fclouds encapsulates the OCCIware Metamodel and helps developers understand without ambiguity the static semantics of cloud environments and the behavioural semantics of their operations. From the developer's perspective, fclouds acts a black box: the developer defines OCCI extensions using OCCIware Studio as entry point of fclouds, and retrieves a formal specification of each extension. This specification is written in Alloy which is a lightweight relational formal language based on the first-order logic. The Alloy syntax is simple and easy to use, and through my experimentation I demonstrated that it is expressive enough to specify different cloud concerns. In addition, by using the Alloy analyzer, developers can check the consistency of their extensions, the sequentiality of certain couples of cloud operations, the reversibility of others, as well as the idempotence and safety of certain operations. If counterexamples are found, the developers can detect inconsistencies in their extensions. Finally, I describe transformation rules for mapping concepts from a cloud solution to another and thus, I make cloud solutions more semantically interoperable.

Together, these two contributions support the automated construction of formal cloud specifications by handling the complexities linked to the natural language documentations of cloud providers. They provide means to specify cloud concepts and operations and a way for verifying their consistency and various other properties. In addition, they provide means for defining transformation rules, thus ensuring semantic interoperability among cloud providers.

Perspectives

In this dissertation, I presented my work that successfully covers the needs of precisely modeling and verifying cloud resources and reasoning over them. However, there is still a lot of work that can be done to improve my research. In this section I thus discuss some short-term and long-term perspectives that should be considered in the continuation of this work.

Short-term Perspectives

Broadening the validation scope of OCCIware. The OCCIware approach was successfully validated by designing and managing, using the OCCIware Studio and the OCCIware Runtime respectively, five OCCI extensions and three academic uses cases. Hereafter, we target industrial validation for the OCCIware approach. Therefore, an ongoing work aims to get this approach tested and adopted within Scalair [scaa], a hybrid cloud provider. Also, in order to cover the whole cloud market, the Xscalibur [xsc] start-up is currently developing the Multi-Cloud Studio1 that supports two other cloud providers: AWS and OpenStack. Both OCCI extensions for AWS and OpenStack are under development2 in order to provide a modeling studio to design both AWS and OpenStack configurations.

Generating a new textual documentation from GCP Model and evaluating it. I aim to generate from GCP Model, thanks to the OCCIware Stu-6.3. Perspectives 157 dio facilities, a new textual documentation of GCP API. Then, I aim to strengthen the validation of this documentation by conducting a survey to be taken by developers that are using GCP API. This survey will help us to verify how accurate the processed documentation is and if it actually saves their development time. Also, for ultimate measurement of our approach, we will contact Google employees who are in charge of GCP API, because we believe that their expertise is the most efficient for reviewing this work.

Providing a complete tool chain for GCP. For the moment, GCP Model is an enhanced and accurate specification of the GCP API that allows the developer to analyze and correctly understand its services. The developer would therefore make more effective use of GCP API and tend to write more efficient code or REST requests. GCP Studio, which is a dedicated model-driven environment for graphically and textually designing configurations that conform to GCP Model, is a work in progress. I aim to associate GCP Studio to a GCP connector in order to allow an effective provisioning of GCP resources and their management at runtime.

Extending the catalog of formal cloud APIs. As described in Chapter 5, I successfully specified thirteen cloud APIs by using my proposed fclouds language. I aim to extend my catalog of formal cloud APIs in order to achieve my vision of building the first comprehensive framework for semantic interoperability in multiclouds. Therefore, using the fclouds language, I aim to formally specify AWS, OpenStack, TOSCA, etc.

Long-term Perspectives

Automatically generating OCCIware deployment plans. We target to extend OCCIware Studio in order to support the automatic generation of deployment plans from OCCI configurations. Currently, the cloud developer does this task manually. This feature allows us to analyze the different resources and links between them available in an OCCI configuration and deduce a deployment plan, which will be automatically executed on OCCIware Runtime.

Following the evolution of GCP API. I plan to update my approach so it would automatically handle the evolution of GCP API. At the moment, this evolution is manually ensured. For automating the process, it is more practical if my crawler is less related to the structure of GCP HTML pages, because in reality the latter are constantly updated. This can be done by experimenting artificial intelligence algorithms to extract knowledge from GCP documentation, then studying whether the inferred GCP Model in this case will not be missing some information. Also, my model needs to incrementally detect streaming modifications, by calculating and modifying only the differences between the initially processed version and the newly modified one.

Dealing with additional types of properties. fclouds allows to verify that the appropriate cloud operations satisfy these five properties: consistency, sequentiality, reversibility, idempotence and safety. For verifying different aspects of the cloud APIs, I aim to enrich fclouds with additional properties such as Reachability, i.e., when executing operations on cloud resources through APIs, there is always a transition from a resource state to another.

Considering further formal techniques. I proposed in this dissertation to use the Alloy formal language and its analyzer to formally specify cloud APIs and reason about them. However, being a SAT solver, Alloy is not effective for resolving numerical constraints which aim for example to minimize the cloud application cost. Therefore, I intend to use adequate heuristics like SMT solvers, which are obviously better than SAT solvers for such scenarios. For example, the TLA+ specification language and TLC, its model checker [Lamport 2002] are recognized and used to verify the reachability problem. Furthermore, although model checkers verify that the properties are valid within a big scope of research, I need to prove it in the absolute through a convincing argument. Hence, I will use automated proof assistants [Loveland 2016], namely Coq [START_REF] Barras | [END_REF]], which implements algorithms and heuristics to build a proof describing the sequence of needed moves in order to solve a property.

Working on real-world interoperability. I presented in Chapter 5, a scenario that showed the usage of fclouds for ensuring semantic interoperability. It mainly consisted in two stages: modeling and reasoning. For the future, I aim to introduce a third stage, where my formal framework is incorporated in the development and maintenance of a bridge with a unified API, to promote real-world interoperability, while formal semantics is properly reflected in its behaviour. This third stage is depicted in (3) of Figure 6.1.

Improving the management of cloud applications. In this thesis, I focused on OCCI standard, which is developed by the OGF and aims to standardize an API for the management of any kind of cloud resources. Besides OCCI, TOSCA currently receives more attention by both the industry and research community, but their focus is different and they can be used complementarily. For managing TOSCA Studio, a dedicated model-driven environment for designing applications with TOSCA. This approach will allow TOSCA to have a complementary tool to take better advantage of deployed applications in production environments. At runtime, TOSCA Studio will be able to: (i) communicate with an OCCI Infrastructure such as the EGI FC to provision virtual machines for example, or (ii) be exposed via the OCCI Plaform API in order to create, retrieve, update and delete any kind of cloud application resources.

Final Conclusion

To close this manuscript, two quotes synthesize the main idea of this thesis:

"No problem can be solved from the same consciousness that created it."

-Albert Einstein

This first quote remarks the value of changing the consciousness to resolve a challenge in life. In other terms, what got you to a problem is not going to get you out of it. Therefore, proposing new cloud APIs to resolve the heterogeneity of the existing ones, will only worsen the problem. However, MDE brings new opportunities to improve the cloud solutions. This thesis evidences the value of rising in abstraction to face the heterogeneity in the cloud domain.

"Concision in style, precision in thought, decision in life."

-Victor Hugo

This second quote remarks the value of concision and precision to successfully make a decision. Eliminating redundancy while conveying the ideas without ambiguity, will lead to a better conclusion. By using formal methods to provide a concise and precise specification mechanism, this thesis evidences a better understanding of cloud APIs. This is crucial for taking efficient use of the cloud ecosystem and for making better decisions regarding the offers selection.

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.2 Background on OCCI . . . . . . . . . . . . . . . . . . . . . . . . . . 53 3.3 OCCIware Approach . . . . . . . . . . . . . . . . . . . . . . . . . . 55 3.3.1 Managing Everything as a Service with OCCIware . . . . . 55 3.3.2 Generating Cloud Domain-Specific Modeling Studios with OCCIware . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 3.4 OCCIware Metamodel . . . . . . . . . . . . . . . . . . . . . . . . . 61 3.5 OCCIware Studio . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 3.6 OCCIware Runtime . . . . . . . . . . . . . . . . . . . . . . . . . . 75 3.7 Evaluation of OCCIware Studio . . . . . . . . . . . . . . . . . . . . 77 3.7.1 Implementation of a Catalog of Standard OGF's OCCI Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 3.7.2 Five OCCIware Use Cases . . . . . . . . . . . . . . . . . . . . 85 3.7.3 Synthesis on the OCCIware Approach . . . . . . . . . . . . 89 3.8 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

Figure 1

 1 Figure 1.1: My Thesis in Comics -Part 1.

Figure 1 . 2 :

 12 Figure 1.2: Thesis Vision.

Figure 1

 1 Figure 1.3: My Thesis in Comics -Part 2.

  Figure 2.1: Multi-Cloud Ecosystem.

Figure 2 . 2 :

 22 Figure 2.2: Taxonomy Criteria.

Contents 3 . 1

 31 Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.2 Background on OCCI . . . . . . . . . . . . . . . . . . . . . . . 53 3.3 OCCIware Approach . . . . . . . . . . . . . . . . . . . . . . 55 3.3.1 Managing Everything as a Service with OCCIware . . . . . 55 3.3.2 Generating Cloud Domain-Specific Modeling Studios with OCCIware . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 3.4 OCCIware Metamodel . . . . . . . . . . . . . . . . . . . . . 61 3.5 OCCIware Studio . . . . . . . . . . . . . . . . . . . . . . . . 71 3.6 OCCIware Runtime . . . . . . . . . . . . . . . . . . . . . . 75 3.7 Evaluation of OCCIware Studio . . . . . . . . . . . . . . . . 77 3.7.1 Implementation of a Catalog of Standard OGF's OCCI Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 3.7.2 Five OCCIware Use Cases . . . . . . . . . . . . . . . . . . . . 85 3.7.3 Synthesis on the OCCIware Approach . . . . . . . . . . . . 89 3.8 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92

FigureFigure 3 . 2 :

 32 Figure 3.1: OCCI Specifications.

  3: (i) OCCIware Studio implemented by Faiez Zalila, and (ii) OCCIware Runtime implemented by Christophe Gourdin.

Figure 3

 3 Figure 3.3: OCCIware Studio and OCCIware Runtime.

  Figure 3.4: Model-Driven Managing Everything as a Service with OCCIware.

Figure 3

 3 Figure 3.5: Generating Cloud Domain-Specific Modeling Studios with OCCIware.

  Figure 3.6: Ecore diagram of OCCIware Metamodel.

  c o n t e x t Mixin i n v a r i a n t N o C y c l i c I n h e r i t a n c e : depends->c l o s u r e ( depends )->e x c l u d e s ( s e l f ) ;

  c o n t e x t FSM i n v a r i a n t A t t r i b u t e T y p e : a t t r i b u t e . type . o c l I s T y p e O f ( EnumerationType ) ;Definition 10 The attribute of a FSM instance must belong to the attributes of the owner Type instance.c o n t e x t FSM i n v a r i a n t A t t r i b u t e M u s t B e D e f i n e d : s e l f . o c l C o n t a i n e r ( ) . oclAsType ( Type ) . a t t r i b u t e s ->i n c l u d e s ( s e l f . a t t r i b u t e )• State is an added concept to model a FSM state of a kind/mixin instance. It can be an initial and/or a final one. It refers to a literal and can own a set of transitions (outgoingTransitions).Definition 11 The enumerationType of a State literal is equals to the type of the attribute of the owner FSM instance.

  c o n t e x t C o n f i g u r a t i o n i n v a r i a n t A l l R e s o u r c e s K i n d s I n U s e : use->i n c l u d e s A l l ( r e s o u r c e s . kind . o c l C o n t a i n e r ( ) ) ;Definition 14 The target resource of all links of all resources of a configuration must be a resource of this configuration.c o n t e x t C o n f i g u r a t i o n i n v a r i a n t A l l Re s o u r c e s L i n k s T a r g e t s I n C o n f i g u r a t i o n : r e s o u r c e s . l i n k s . t a r g e t ->f o r A l l ( r | r . o c l C o n t a i n e r ( ) = s e l f ) ; • Resource is an OCCI Core Model concept and represents any cloud computing resource, such as a virtual machine, a network, and an application. A Resource owns a set of links. Definition 15 The kind of a Resource instance must inherit from the resource kind instance directly or transitively. Resources with OCCIware c o n t e x t R e s o u r c e i n v a r i a n t R e s o u r c e K i n d I s I n P a r e n t : kind->c l o s u r e ( p a r e n t )->e x i s t s ( k | k . term = ' r e s o u r c e ' and k . scheme = ' h t t p : // schemas . o g f . o r g / o c c i / c o r e# ' ) ;

  c o n t e x t R e s o u r c e i n v a r i a n t R e s o u r c e K i n d I s I n P a r e n t :kind->c l o s u r e ( p a r e n t )->e x i s t s ( k | k . term = ' l i n k ' and k . scheme = ' h t t p : // schemas . o g f . o r g / o c c i / c o r e# ' ) ;

  c o n t e x t R e s o u r c e i n v a r i a n t KindCompatibleWithOneAppliesOfEachMixin : p a r t s . mixin->f o r A l l (m | m. a p p l i e s ->notEmpty ( ) implies m. a p p l i e s ->e x i s t s ( k | kind->c l o s u r e ( p a r e n t )->i n c l u d e s ( k ) ) ) ;

Figure 3 . 7 :

 37 Figure 3.7: OCCIware Studio Features.

  Figure 3.8, designing a new OCCI extension consists in extending the OCCI Core extension. Designing an OCCI configuration consists in defining an instance of an OCCI extension and represents a cloud architecture already deployed or to deploy.

Figure 3 . 8 :

 38 Figure 3.8: Projection of OCCI to EMF.

  (i) OCCI HTTP Protocol[Nyrén 2016a], (ii) OCCI Text Rendering[Edmonds 2016], OCCI JSON Rendering[Nyrén 2016d] based on the Jackson 6 library, and (iii) OCCI Core Model[Nyrén 2016b] based on the OCCIware Metamodel. • OCCI Extensions that represent the OCCIware-based modeling of concrete cloud domains such as OCCI Infrastructure [Nyrén 2016c], OCCI corresponding OCCI extension. It executes CRUD (Create, Retrieve, Update and Delete) operations and extension-specific actions, such as start compute for the OCCI Infrastructure extension. The OCCIware Runtime is extensible by design: supporting a new kind of cloud resources consists of adding a new connector.

Figure 3 .

 3 Figure 3.10: OCCI Infrastructure Extension Model.

Figure 3 .

 3 Figure 3.11: An Infrastructure Configuration Model.

  Figure 3.12 shows a generated OCCI configuration model from the Infrastructure configuration model. As shown in the palette of the Infrastructure Designer (right part of Figure 3.11), the Infrastructure Designer allows cloud developers to create an instance of Infrastructure Metamodel such as Compute, Network, and Storage. However, in the palette of the OCCIware Designer (right part of Figure 3.12), the cloud developer can only create instances of OCCIware Metamodel Resource and Link classes.

Figure 3 .

 3 Figure 3.12: An OCCI Configuration Model.

Figure 3 .

 3 Figure 3.13: OCCI CRTP Extension Model.

Figure 3 .

 3 Figure 3.14: OCCI Platform Extension Model.

Figure 3 .

 3 Figure 3.16: OCCI Monitoring Extension Model.

Chapter 3 .

 3 Modeling, Verifying, Generating and Managing Cloud Resources with OCCIware memory, the percentage of used disk, and the average of the CPU utilization. 3.7.2.2 Cloud Mobile Robotics with OCCIware This use case [Merle 2017] illustrates the convergence of cloud computing and robotics platforms. It introduces Open Mobile Cloud Robotics Interface (OMCRI), a Robot-as-a-Service vision based platform, which offers a unified easy access to remote heterogeneous mobile robots. OMCRI is a new OCCI extension for mobile cloud robotics. This extension defines three kinds of heterogeneous robots: Lego Mindstorm NXT 2, Turtlebot, and Parrot AR.Drone. It introduces a set of mixins that customize the sensors and the actuators of each robot. An OMCRI connector has been developed and deployed on the OCCIware Runtime. End users can create OMCRI configuration models to manage the mobile robots. They interact with mobile robots by sending OCCI HTTP requests to the OCCIware Runtime.

Figure 3 .

 3 Figure 3.18: Docker Designer.

Figure 3 .

 3 Figure 3.19: LAMP Designer.

Figure 3 .

 3 Figure 3.20: OCCIware Studio Product Line.

  Figure 4.1, and also outlines the foundations behind it, namely web crawling, cloud modeling and NLP. First, my proposed system takes a documentation as input, and then uses the documentation Specific Parser, Model Generator, Text Analysis Engine and Model Validator to correctly generate the model of the cloud API.

Figure 4

 4 Figure 4.1: My Model Extraction Approach Overview.

Figure 4 . 2 :

 42 Figure 4.2: Different Documentation Formats.

Figure 4

 4 Figure 4.3: Imprecise String Types.

Figure 4

 4 Figure 4.4: Informal Enumeration Types.

Figure 4 . 5 :

 45 Figure 4.5: Error in Describing the "Kind" Attribute.

  Figure 4.6: "Optional/Required" Attribute Constraint.

  Figure 4.7: "Immutable Attribute" Constraint.

  Figure 4.8).

Figure 4

 4 Figure 4.8: "Default Value" Constraint.

Figure 4

 4 Figure 4.9: Hidden Link between Instance and Network.

Figure 4 .

 4 Figure 4.10: GCP Model Extraction Approach Overview.

  Figure 4.11: Metamodeling Stack for GCP Model.

Figure 4 .

 4 Figure 4.12: The Algorithm of the Model Extraction Approach.

Figure 4 .

 4 Figure 4.13: A Subset of OCCIware Metamodel.

Figure 4 .

 4 Figure 4.14: Syntactic Parse Tree for Identifying a Hidden Link in a Sentence.

  Figure 4.15 shows the graphical output of a subset of GCP Model. This diagram also shows an example of Redundancy Removal, where I introduce an abstractKind instance and I factorize the attributes and actions of two versions of the same kind. Further information regarding the abstractKind instance is given in Section 4.4.1.2.

Figure 4 .

 4 Figure 4.15: A Subset of GCP Extension Diagram.

Figure 4 .

 4 Figure 4.16: Recursive Parsing Example.

Figure 4

 4 Figure 4.17: Two Clusters of Development Teams.

Contents 5 . 1

 51 Exploring the Semantic Space . . . . . . . . . . . . . . . . . . 123 5.1.1 Formal methods and their benefits . . . . . . . . . . . . . . . 123 5.1.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 124 5.2 The fclouds Framework . . . . . . . . . . . . . . . . . . . . . 125 5.2.1 Usage Scenario . . . . . . . . . . . . . . . . . . . . . . . . . . 125 5.2.2 Overall Architecture . . . . . . . . . . . . . . . . . . . . . . . 126 5.3 The fclouds Language . . . . . . . . . . . . . . . . . . . . . . 128 5.3.1 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 5.3.2 Specifying fclouds Static Semantics . . . . . . . . . . . . . 129 5.3.3 Specifying fclouds Operational Semantics . . . . . . . . . . 135 5.3.4 Identifying & Validating fclouds Properties . . . . . . . . . 139 5.4 Evaluation of fclouds . . . . . . . . . . . . . . . . . . . . . . 143 5.4.1 Catalog of Cloud Formal Specifications . . . . . . . . . . . . 144 5.4.2 Implementation of fclouds Formal Specifications . . . . . . 147 5.4.3 Verification of fclouds Properties . . . . . . . . . . . . . . . 148 5.4.4 Definition & Validation of Domain-Specific Properties . . . . 148 122 Chapter 5. Specifying Heterogeneous Cloud Resources and Reasoning over them with fclouds 5.4.5 Transformation Rules for Semantic Interoperability in Multiclouds . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 5.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149

  Figure 5.1: Semantic Space.

5. 2 .Figure 5 . 2 :

 252 Figure 5.2: fclouds Usage Scenario.

  Figure 5.3: fclouds Framework Overview.

  Figure 5.4: Formalization Process.

  s i g A t t r i b u t e { name : one S t r i n g , mutable : l o n e Boolean , r e q u i r e d : l o n e Boolean , d e f a u l t : l o n e S t r i n g , d e s c r i p t i o n : l o n e S t r i n g , type : l o n e DataType , m u l t i p l e _ v a l u e s : l o n e Boolean }

  s i g C o n f i g u r a t i o n { u s e : s e t Extension , r e s o u r c e s : s e t Resource -> Time , m i x i n s : s e t Mixin -> Time }

  a l l t : Time | r e s o u r c e s . t . kind . e x t e n s i o n i n u s e

  pred C r e a t e R e s o u r c e [ c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , kind : Kind , m i x i n s : s e t Mixin , a t t r i b u t e s : s e t A t t r i b u t e S t a t e , t , t ' : Time ] { // p r e c o n d i t i o n s a t i n s t a n t t no r e s o u r c e : c o n f i g . r e s o u r c e s . t | r e s o u r c e . i d = r e s o u r c e I d kind i n c o n f i g . u s e . k i n d s m i x i n s i n c o n f i g . u s e . m i x i n s // p o s t c o n d i t i o n s a t i n s t a n t t ' one r e s o u r c e : Resource { r e s o u r c e . i d = r e s o u r c e I d r e s o u r c e . kind = kind r e s o u r c e . m i x i n s . t ' = m i x i n s r e s o u r c e . a t t r i b u t e s . t ' = a t t r i b u t e s c o n f i g . r e s o u r c e s . t ' = c o n f i g . r e s o u r c e s . t + r e s o u r c e } c o n f i g . m i x i n s . t ' = c o n f i g . m i x i n s . t ' }

  pred R e t r i e v e R e s o u r c e [ c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , t , t ' : Time ] { // p r e c o n d i t i o n s a t i n s t a n t t one r e s o u r c e : c o n f i g . r e s o u r c e s . t { r e s o u r c e . i d = r e s o u r c e I d } // p o s t c o n d i t i o n s a t i n s t a n t t ' one r e s o u r c e : c o n f i g . r e s o u r c e s . t ' { r e s o u r c e . i d = r e s o u r c e I d r e s o u r c e . m i x i n s . t ' = r e s o u r c e . m i x i n s . t r e s o u r c e . a t t r i b u t e s . t ' = r e s o u r c e . a t t r i b u t e s . t r e s o u r c e . l i n k s . t ' = r e s o u r c e . l i n k s . t } c o n f i g . r e s o u r c e s . t ' = c o n f i g . r e s o u r c e s . t c o n f i g . m i x i n s . t ' = c o n f i g . m i x i n s . t }

  r e c o n d i t i o n s a t i n s t a n t t one r e s o u r c e : c o n f i g . r e s o u r c e s . t | r e s o u r c e . i d = r e s o u r c e I d & & r e s o u r c e . a t t r i b u t e s . t = a t t r i b u t e 1 a t t r i b u t e 1 ! = a t t r i b u t e 2 // p o s t c o n d i t i o n s a t i n s t a n t t ' one r e s o u r c e : c o n f i g . r e s o u r c e s . t { r e s o u r c e . a t t r i b u t e s . t ' = r e s o u r c e . a t t r i b u t e s . t ++ a t t r i b u t e 2 138 Chapter 5. Specifying Heterogeneous Cloud Resources and Reasoning over them with fclouds } c o n f i g . r e s o u r c e s . t ' = c o n f i g . r e s o u r c e s . t c o n f i g . m i x i n s . t ' = c o n f i g . m i x i n s . t }

  pred D e l e t e R e s o u r c e [ c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , t , t ' : Time ] { // p r e c o n d i t i o n s a t i n s t a n t t one r e s o u r c e : c o n f i g . r e s o u r c e s . t | r e s o u r c e . i d = r e s o u r c e I d // p o s t c o n d i t i o n s a t i n s t a n t t ' one r e s o u r c e : c o n f i g . r e s o u r c e s . t { r e s o u r c e . i d = r e s o u r c e I d c o n f i g . r e s o u r c e s . t ' = c o n f i g . r e s o u r c e s . tr e s o u r c e } c o n f i g . m i x i n s . t ' = c o n f i g . m i x i n s . t }

  a s s e r t C r e a t e R e s o u r c e I s C o n s i s t e n t { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , r e s o u r c e K i n d : Kind , m i x i n s : Mixin , a t t r i b u t e s : A t t r i b u t e S t a t e , t : Time | C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , r e s o u r c e K i n d , mixins , a t t r i b u t e s , t , t . next ] i m p l i e s { no r e s o u r c e : c o n f i g . r e s o u r c e s . t | r e s o u r c e . i d = r e s o u r c e I d r e s o u r c e K i n d i n c o n f i g . u s e . k i n d s and one r e s o u r c e : c o n f i g . r e s o u r c e s . ( t . next ) | r e s o u r c e . i d = r e s o u r c e I d and r e s o u r c e . kind = r e s o u r c e K i n d } } a s s e r t D e l e t e R e s o u r c e R e v e r s e C r e a t e R e s o u r c e { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , kind : Kind , m i x i n s : Mixin , a t t r i b u t e s : A t t r i b u t e S t a t e , t : Time { C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , kind , mixins , a t t r i b u t e s , t , t . next ] i m p l i e s D e l e t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , t . next , t ] } }

  a s s e r t C r e a t e R e s o u r c e T h e n R e t r i e v e R e s o u r c e { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , kind : Kind , m i x i n s : s e t Mixin , a t t r i b u t e s : s e t A t t r i b u t e S t a t e , t : Time | C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , kind , mixins , a t t r i b u t e s , t , t . next ] and R e t r i e v e R e s o u r c e [ c o n f i g , r e s o u r c e I d , t . next , t . next . next ] i m p l i e s one r e s o u r c e : c o n f i g . r e s o u r c e s . ( t . next . next ) { r e s o u r c e . i d = r e s o u r c e I d and r e s o u r c e . kind = kind and r e s o u r c e . m i x i n s . ( t . next . next ) = m i x i n s } }

  a s s e r t C r e a t e R e s o u r c e I s I d e m p o t e n t { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , kind : Kind , m i x i n s : Mixin , a t t r i b u t e s : A t t r i b u t e S t a t e , t : Time | C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , kind , mixins , a t t r i b u t e s , t , t . next ] and C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , kind , mixins , a t t r i b u t e s , t . next , t . next . next ] i m p l i e s c o n f i g . r e s o u r c e s . ( t . next ) = c o n f i g . r e s o u r c e s . ( t . next . next ) }

  a s s e r t U p d a t e R e s o u r c e I s I d e m p o t e n t

  a s s e r t R e t r i e v e R e s o u r c e I s S a f e { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , t : Time | R e t r i e v e R e s o u r c e [ c o n f i g , r e s o u r c e I d , t , t . next ] i m p l i e s c o n f i g . r e s o u r c e s . t = c o n f i g . r e s o u r c e s . ( t . next ) and c o n f i g . m i x i n s . t = c o n f i g . m i x i n s . ( t . next ) and one r e s o u r c e : c o n f i g . r e s o u r c e s . ( t . next ) { r e s o u r c e . i d = r e s o u r c e I d r e s o u r c e . a t t r i b u t e s . t = r e s o u r c e . a t t r i b u t e s . ( t . next ) r e s o u r c e . l i n k s . t = r e s o u r c e . l i n k s . ( t . next ) } }

Figure 5

 5 Figure 5.5: Alloy Generator.

Figure 5

 5 Figure 5.6: Acceleo Template.

  Summary . . . . . . . . . . . . . . . . . . . . . . 153 6.2 Contributions Summary . . . . . . . . . . . . . . . . . . . . . 154 6.3 Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156 6.3.1 Short-term Perspectives . . . . . . . . . . . . . . . . . . . . . 156 6.3.2 Long-term Perspectives . . . . . . . . . . . . . . . . . . . . . 157 6.4 Final Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . 159

  Figure 6.1: Formal Real-World Bridge.

  1.1 Thesis Context . . . . . . . . . . . . . . . . . . . . . . . . . . .

6 1.2 Problem Statement . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Research Questions . . . . . . . . . . . . . . . . . . . . . . . . 9 1.4 Thesis Goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.5 Thesis Vision . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.6 Proposed Solution . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.7 Dissertation Roadmap . . . . . . . . . . . . . . . . . . . . . . 14 1.8 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.8.1 International Conferences . . . . . . . . . . . . . . . . . . . . 16 1.8.2 International Journal . . . . . . . . . . . . . . . . . . . . . . . 17 1.9 Awards . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

Table 2 .

 2 1: Heterogeneity of Cloud Providers.

	Cloud Provider Deployment Model Service Model CRM-API
	AWS [aws]	Public	IaaS & PaaS REST & SOAP
	DigitalOcean [dig]	Public	IaaS	REST
	EGI FC [egi]	Private	IaaS	REST
	FlexiScale [fle]	Public	IaaS	SOAP
	GCP [gcp]	Public	IaaS & PaaS	REST
	Microsoft Azure [azu]	Hybrid	IaaS	REST
	Heroku [her]	Public	PaaS	REST
	SalesForce [sal]	Public	SaaS	REST & SOAP
	VMware [vmw]	Hybrid	IaaS	REST

Table 2 .

 2 2: MDAC Usages.

	MDAC	Design Time Deployment Time Production Time
	Blueprinting
	Brooklyn
	CAMEL
	CAML
	Cloud Adoption Toolkit
	Cloud DSL
	CloudGenius
	CloudMIG
	CloudML
	Farokhi
	Frey et al.
	Garcia-Galán et al.
	Gherardi et al.
	Holmes
	MOCCA
	MULTICLAPP
	OpenTOSCA
	RESERVOIR-ML
	SALOON
	soCloud
	Sousa et al.
	StratusML

Table 2 .

 2 3: MDAC Concepts.

	MDAC	Service Model
	Blueprinting	XaaS
	Brooklyn	PaaS
	CAMEL	XaaS
	CAML	IaaS & PaaS
	Cloud Adoption Toolkit	IaaS
	Cloud DSL	IaaS
	CloudGenius	IaaS
	CloudMIG	IaaS & PaaS
	CloudML	IaaS & PaaS
	Farokhi	IaaS & SaaS
	Frey et al.	IaaS
	Garcia-Galán et al.	IaaS
	Gherardi et al.	RaaS
	Holmes	IaaS
	MOCCA	IaaS
	MULTICLAPP	PaaS
	OpenTOSCA	IaaS & PaaS
	RESERVOIR-ML	IaaS
	SALOON	IaaS & PaaS
	soCloud	IaaS & PaaS
	Sousa et al.	PaaS
	StratusML	IaaS

Table 2 .

 2 4: CML Characteristics.

	MDAC Blueprinting Brooklyn CAMEL CAML Cloud Adoption Toolkit Cloud DSL CloudGenius CloudMIG CloudML Farokhi Frey et al. Garcia-Galán et al. Gherardi et al. Holmes MOCCA MULTICLAPP OpenTOSCA RESERVOIR-ML Components Paradigm Services & Components Components Services & Components Services & Components Services Services & Components Services Components Services & Components Services & Components Services & Components Feature Models Feature Model Services & Components Components Services & Components Services & Components & Resources SALOON Feature Models soCloud Services & Components Sousa et al. Feature Models StratusML Services & Components	Abstract Syntax XML schema YAML document Ecore UML profile UML profile Ecore Ecore Ecore Ecore XML schema UML profile -Ecore Ecore Ecore UML profile XML schema or YAML document XML schema Ecore XML schema Ecore Microsoft DSL	Concrete Syntax Graphical Textual Textual Graphical Graphical Graphical Textual Textual Textual Textual Graphical Graphical Graphical & Textual Textual Graphical & Textual Graphical Graphical & Textual Graphical Graphical Textual Textual Graphical	Semantics Natural language Natural language & CAMP specification Natural language & ExecutionWare Natural language Natural language Mapping to TOSCA Natural language & Selection Framework Natural language & CloudMIG Xpress (Deployment Optimizer) Natural language & CloudMF Service Selection Engine Natural language & CDO Xpress (Deployment Optimizer) Natural language & Automated Analysis of Feature Models (AAFM) Resolution Engine Natural language Natural language & Deployment Optimizer Natural language & Deployment Engine Natural language & TOSCA specification Natural language & OpenNebula An Ontology & Translation into a constraint solver Natural language & FraSCAti Temporal constraints Natural language

Table 3 .

 3 1: The Mapping Process of OCCI Concepts into EMF Concepts. Alloy analyzer. The Alloy analyzer is a solver that takes the constraints of a model and finds structures that satisfy them. We used it to explore the model by generating sample OCCI configurations, and also to check properties of the OCCI extension by generating counterexamples.

	OCCI concept EMF concept
	Kind	EClass
	Kind's source	OCL invariant
	Kind's target	OCL invariant
	Attribute	EAttribute
	Action	EOperation
	Mixin	EClass
	Constraint	OCL invariant
	BasicType	EDataType
	EnumerationType EEnum
	RecordType	EClass
	ArrayType	EClass
	extensions formally with the

Table 3 . 2 :

 32 OCCIware Use Cases

		Infrastructure	Simulation	OMCRI	Docker	MoDMaCAO	GCP	Coverage
	Cloud Domain	IaaS	IaaS	RaaS	CaaS	PaaS	[I P S]aaS XaaS
	Design Verification Documentation Code generation Model interpretation Deployment Discovery Management Monitoring	VMware API	CloudSim API	Robots API	Docker API	Ansible API	GCP API

Table 4

 4

		Before Abstraction	After Abstraction
	Redundant Attributes	# of occurrences	% of redundancy	# of occurrences	% of redundancy
	name id selfLink kind description	92 80 79 79 75	64,79% 56,34% 55,63% 55,63% 52,82%	26 14 13 13 9	18,31% 9,86% 9,15% 9,15% 6,34%
	Average		57,04%		10,56%
	Redundant Actions	# of occurrences	% of redundancy	# of occurrences	% of redundancy
	get list delete insert Average	142 142 140 76	100,00% 100,00% 98,59% 53,52% 88,02%	76 76 74 10	53,52% 53,52% 52,11% 7,04% 41,54%

.1: Redundant Attributes and Actions among Kinds.

Table 4 .

 4

	2: GCP Products. Number of Resources 48 2 1 Cloud User Account Product Name App Engine BigQuery Cloud Functions 2 Management Offered Service Compute Big Data Compute Compute Engine 67 Compute Container Engine 1 Compute Cloud Dataproc 4 Big Data Cloud DNS 1 Network Cloud IAM 2 Identity & Security Logging 2 Management Cloud Pub/Sub 2 Big Data Runtime Config 3 Management Cloud SQL 2 Storage & Databases Cloud Storage 5 Storage & Databases Total 142 6

  Table 4.3 presents a summary of my GCP Model.This dataset covers all the information presented in GCP official documentation and formalized by GCP Model. For each class of my model, Table4.3 provides the number of instances present in my dataset. The last line provides the total of GCP objects present in the dataset.

	Chapter 4. Inferring Precise Models from Cloud APIs Textual
		Documentations
	Table 4.3: Summary of the GCP Model Dataset.
	GCP	GCP
	Metaclass Name	Model Instances
	Kind	142
	Attribute	2124
	Action	985
	BooleanType	90
	NumericType	375
	StringType	1402
	ArrayType	218
	EnumerationType	21
	EnumerationLiteral	80
	RecordType	143
	RecordField	613
	Total	5437

A

  Resource instance owns a set of mutable links.• Link is the relationship between two Resource instances. For example,NetworkInterface connects a Compute instance to a Network instance, and StorageLink connects a Compute instance to a Storage instance.

	s i g Resource e x t e n d s E n t i t y {
	l i n k s : s e t Link -> Time
	}
	s i g Link e x t e n d s E n t i t y {
	s o u r c e : Resource one -> Time ,
	t a r g e t : Resource one -> Time
	}

Table 5 .

 5 1: fclouds Static Semantics.

	fclouds Concepts	Description
	an abstract type defining the set of all resources and links an immutable type of OCCI entities AttributeState an instantiated OCCI attribute Entity Kind an entity property, Attribute such as the hostname of a virtual machine
	DataType Mixin Action	an abstract type defining enumerations, lists, records, etc. represents crosscutting attributes and actions that can be dynamically added to an OCCI entity domain specific behavior, such as start/stop a virtual machine
	Category Resource	the abstract base class inherited by Kind, Mixin and Action represents any cloud computing resource, such as a virtual machine
	Link Extension	a relation between two resources a concrete cloud computing domain, such as IaaS, PaaS, SaaS, cloud robotics, etc.
	Configuration	a running OCCI system

Table 5

 5

.1 presents a summary of the fclouds language concepts.

  2 . 1. OCCI Infrastructure [Nyrén 2016c] is an OCCI-based extension for IaaS application domain. It defines compute, storage and network resource types and associated links. It defines five kinds such as Compute, six mixins such as IpNetworkInterface, and around twenty data types such as Vlan range. The Compute kind represents a generic information processing resource, e.g., a virtual machine or container. It inherits the Resource kind defined in the OCCI Core Model. Compute has a set of OCCI attributes that I declare as fields to my Compute signature, such as occi.compute.architecture to specify the CPU architecture of the instance, occi.compute.core to define the number of virtual CPU cores assigned to the instance, occi.compute.memory to define the maximum RAM in gigabytes allocated to the instance, etc. The lone keyword signifies that the relation between two tuples from two sets, such as occi.compute.architecture and Architecture, has a 0..1 cardinality.

	s i g Compute e x t e n d s f c l o u d s / Resource {
	o c c i _ c o m p u t e _ a r c h i t e c t u r e : l o n e A r c h i t e c t u r e ,
	occi_compute_cores : l o n e Core ,
	occi_compute_hostname : l o n e S t r i n g ,
	occi_compute_share : l o n e Share ,
	occi_compute_speed : l o n e GHz,
	occi_compute_memory : l o n e GiB ,
	occi_compute_state : one ComputeStatus ,
	occi_compute_state_message : l o n e S t r i n g
	}

Table 5 .

 5 3: Summary of the fclouds Framework Dataset. OCCI CRTP[START_REF] Drescher | [END_REF]] is an OCCI-based extension that defines a set of preconfigured instances of the OCCI Compute resource type.3. Docker is a lightweight container for deploying and managing applications.Docker is implemented as an extension of OCCI in[START_REF] Paraiso | Model-driven Management of Docker Containers[END_REF]]. It defines generic and specific container and machine resource types and associated links. 4. GCP is one of the leaders among cloud providers. It offers several service such as Compute, Storage, Network, Management, Big Data and Security. GCP was implemented as OCCI extension in [Challita 2018a] and as I presented in Chapter 4. I present in the following the formal specification of the Instance resource type, which represents a virtual machine in GCP. s i g I n s t a n c e e x t e n d s f c l o u d s / Resource { creationTimestamp : one S t r i n g , name : one S t r i n g , d e s c r i p t i o n : one S t r i n g , machineType : one S t r i n g , s t a t u s : one StatusEnum , s t a t u s M e s s a g e : one S t r i n g , zone : one S t r i n g d i s k s : one DiskRecord , over them with fclouds cpuPlatform : one S t r i n g , l a b e l s : one Map, minCpuPlatform : one S t r i n g , g u e s t A c c e l e r a t o r s : one G u e s t A c c e l e r a t o r R e c o r d , s t a r t R e s t r i c t e d : one Boolean , d e l e t i o n P r o t e c t i o n : one Boolean , kind : one S t r i n g } 5. VMware is a virtualization and cloud computing software provider and it is implemented as an extension of OCCI in [Zalila 2017b]. It defines VMware instance, storage and network resource types and associated links. 6. OCCI Platform [Metsch 2016] is an OCCI-based extension for PaaS application domain. It defines application and component resource types and associated links. 7. MoDMaCAO [Korte 2018] is an application of OCCI for managing cloud applications. It defines generic and specific application, component, installation dependency and execution dependency resource types.

	Extension	#Kind #Mixin #Attribute #Action #DataType
	IaaS
	OCCI Infrastructure OCCI CRTP Docker GCP VMware	5 0 24 150 6	6 6 0 0 7	31 18 251 2348 19	9 0 7 985 0	20 0 2 398 1
	PaaS
	OCCI Platform MoDMaCAO	3 1	4 31	11 9	4 0	3 2
	IoT
	OMCRI CoT	5 6	9 4	20 21	15 0	2 3
	Transverse
	cloud concerns
	OCCI SLA	2	2	8	5	4
	OCCI Monitoring	2	3	9	0	2
	Cloud Simulation	8	14	53	0	0
	Cloud Elasticity Total	2 214	4 90	23 2821	4 1029	5 442
	2.

Inferring Precise Models from Cloud APIs Textual Documentations

WSDL is an Extensible Markup Language (XML)-based language that is used for describing the functionality offered by a Web service.

SOAP is a protocol specification for exchanging structured information in the implementation of Web Services in computer networks.

UDDI is a platform-independent, XML-based registry by which businesses worldwide can list themselves on the Internet, and a mechanism to register and locate Web service applications.

www.occiware.org

Available here https://github.com/occiware/OCCI-Studio/blob/master/plugins/org. eclipse.cmf.occi.core/model/OCCI.ecore

https://github.com/EGI-FCTF/jOCCI-api

https://github.com/occiware/MartServer

https://github.com/FasterXML/jackson

https://github.com/occiware/OCCI-Studio/blob/master/plugins/org.eclipse.cmf. occi.infrastructure/model/Infrastructure.occie

https://github.com/occiware/OCCI-Studio/tree/master/plugins/org.eclipse.cmf. occi.infrastructure

https://github.com/occiware/OCCI-Studio/tree/master/plugins/org.eclipse.cmf. occi.CRTP

https://github.com/occiware/OCCI-Studio/tree/master/plugins/org.eclipse.cmf. occi.platform

https://github.com/occiware/OCCI-Studio/tree/master/plugins/org.eclipse.cmf. occi.sla

https://github.com/occiware/OCCI-Studio/tree/master/plugins/org.eclipse.cmf. occi.monitoring

Available here https://github.com/occiware/Docker-Studio

Available here https://github.com/occiware/OCCI-Studio/tree/master/plugins/org. eclipse.cmf.occi.infrastructure/documentation

Available here https://github.com/occiware/Multi-Cloud-Studio/tree/master/plugins/ org.eclipse.cmf.occi.multicloud.vmware

https://cloud.google.com

https://cloud.google.com/deployment-manager/docs/configuration/ supported-resource-types

https://jsoup.org

https://github.com/occiware/GCP-Model

https://github.com/occiware/fclouds-Framework

https://github.com/occiware/fclouds-Framework

https://github.com/occiware/Multi-Cloud-Studio

Available here https://github.com/occiware/Multi-Cloud-Studio/tree/master/plugins/ org.eclipse.cmf.occi.multicloud.aws.ec2

Acknowledgments

State of the Art

In this part, I review approaches related to cloud computing and I classify the existing models for the cloud.

Platform [START_REF] Metsch | [END_REF]], OCCI SLA [Katsaros 2016], Docker [START_REF] Paraiso | Model-driven Management of Docker Containers[END_REF]], cloud mobile robotics [Merle 2017], etc.

Figure 3.9: OCCIware Runtime Architecture.

• OCCI Configurations that are instances of OCCIware configuration, such as a configuration using OCCI Infrastructure and containing a running virtual machine with 4 cores, 3.2 GHz and 16 GiB.

• OCCI Connectors that consist in the pivot between OCCIware extensions/configurations and CRM-APIs. Each connector is dedicated to a specific cloud domain, e.g., AWS, GCP, Docker, or mobile robotics. It implements the example, the following OCL constraint specifies that each Network instance must have a unique VLAN.

i n v UniqueVlan : Network . a l l I n s t a n c e s ( )->i s U n i q u e ( o c c i . network . v l a n )

In addition, we define, in the following, an additional OCL constraint in the IpNetworkInterface mixin, which checks that all IP addresses must be different. Once the extension is defined, the generation process of Infrastructure Tooling may be triggered. It generates four main elements: (i) the Infrastructure Metamodel, (ii) the Java-based Infrastlandscructure Implementation, (iii) Infrastructure Connector, and (iv) Infrastructure Designer.

Listing 3.1 shows a subset of the generated Network connector class. It extends the NetworkImpl class generated by the EMF tooling and contains the OCCI specific callback methods for the CRUD operations and all Network kind-specific actions (i.e., up and down). The generated code of specific actions is deducted from the defined FSM on the Network kind.

Contributions

In the end of Part II, I discussed the need of automatically building cloud models and formally reasoning over them. In this part, I detail my solution to make it reality.

Chapter 4

Inferring Precise Models from Cloud APIs Textual Documentations

This chapter is an extended version of our paper "A Precise Model for Google Cloud Platfom" [Challita 2018a] Note that to model finite execution traces, Alloy defines a library util/ordering that provides useful relations to manipulate the total order of Time concept, namely first to denote the first time, and next, a binary relation that, given a time returns the following time in the order.

The fclouds static semantics and all OCCI REST operations were proven to be consistent, as shown in Table 5.2. However, the notion of consistency is basic and does not suffice in order to validate my fclouds language. There are other examples of reliable verification and validation tasks that can be performed on pairs of operations such as sequentiality and/or reversibility of operations.

Reversibility

Two cloud API operations are reversible when they contain inverse mathematical logic. For example, de-provisioning a virtual machine reverses the operation of provisioning it. In OCCI, Create Resource and Delete Resource, Create Link and Delete Link are reversible. The following assertion, which is checking that Create Resource is reversed by Delete Resource, was proven to be valid.

Verification of fclouds Properties

Being rigorously encoded using the same formal language, i.e., fclouds, my thirteen case studies can be now accessed by the same OCCI RESTful interface. Therefore, it is important to make sure that they correctly reflect the behaviour of fclouds. Using the Alloy analyzer, I verify that my thirteen formal specifications satisfy all the assertions, i.e., properties, that I formulated in my fclouds language (cf. Table 5.2). For instance, I verify that Create Compute operation of OCCI Infrastructure is idempotent and that Update Instance operation of GCP is not safe.

Definition & Validation of Domain-Specific Properties

My framework allows me to verify some domain-specific properties. For instance, in the following listing, I check whether creating a NetworkInterface between two OCCI resources only occurs between one Compute resource type and one Network resource type. This assertion is validated so my formal specification respects and implements the following requirement of OCCI Infrastructure specification: "Net-workInterface connects a Compute instance to a Network instance" [Nyrén 2016c].

Conclusion

The last part of the manuscript presents a summary, future perspectives and final remarks of this thesis.