Inferring Models from Cloud APIs and Reasoning over Them: A Tooled and Formal Approach

Stéphanie Challita 1, 2
2 SPIRALS - Self-adaptation for distributed services and large software systems
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Abstract : 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 model-driven 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.
Complete list of metadatas

Cited literature [175 references]  Display  Hide  Download

https://tel.archives-ouvertes.fr/tel-02016442
Contributor : Stéphanie Challita <>
Submitted on : Wednesday, February 13, 2019 - 2:29:48 PM
Last modification on : Friday, May 17, 2019 - 11:40:52 AM
Long-term archiving on : Tuesday, May 14, 2019 - 1:01:14 PM

File

Challita-Thesis-final.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02016442, version 1

Citation

Stéphanie Challita. Inferring Models from Cloud APIs and Reasoning over Them: A Tooled and Formal Approach. Software Engineering [cs.SE]. Universite Lille 1, 2018. English. ⟨tel-02016442⟩

Share

Metrics

Record views

215

Files downloads

547