Inferring models from cloud APIs and reasoning over them : a tooled and formal approach
(Inférer des modèles à partir d'APIs cloud et raisonner dessus : une approche outillée et formelle)

URL d'accès : http://ori-nuxeo.univ-lille1.fr/nuxeo/site/esupver...

Auteur(s):  Challita, Stéphanie
Date de soutenance : 21/12/2018
Éditeur(s) : Université Lille1 - Sciences et Technologies 

Langue : Anglais
Directeur(s) de thèse :  Merle, Philippe
Laboratoire : Centre de recherche en informatique, signal et automatique de Lille (CRIStAL)
Ecole doctorale : École doctorale Sciences pour l'Ingénieur (Lille)

Classification : Informatique
Discipline : Informatique et applications
Mots-clés : Multi-nuages
Open Cloud Computing Interface (OCCI)
Google Cloud Platform
Alloy
Langage dédié
Informatique dans les nuages
Ingénierie dirigée par les modèles
Rétro-ingénierie (informatique)
Méthodes formelles (informatique)
Langages formels
Vérification de modèles (informatiques)

Résumé : Avec l’avènement de l’informatique en nuage, différents fournisseurs offrant des services en nuage et des interfaces de programmation d’applications (APIs) hétérogènes sont apparus. Cette hétérogénéité complique la mise en œuvre d’un système de multi-nuages interopérable. Parmi les solutions pour l’interopérabilité de multi-nuages, l’Ingénierie Dirigée par les Modèles (IDM) s’est révélée avantageuse. Cependant, la plupart des solutions IDM existantes pour l’informatique en nuage ne sont pas représentatives des APIs et manquent de formalisation. Pour remédier à ces limitations, je présente dans cette thèse une approche basée sur le standard Open Cloud Computing Interface (OCCI), les approches IDM et les méthodes formelles. Je fournis deux contributions qui sont mises en œuvre dans le contexte du projet OCCIware. Premièrement, je propose une approche basée sur la rétro-ingénierie pour extraire des connaissances des documentations textuelles ambiguës des APIs de nuages et améliorer leur représentation à l’aide des techniques IDM. Cette approche est appliquée à Google Cloud Platform (GCP), où je propose GCP Model, une spécification précise et basée sur les modèles, automatiquement déduite de la documentation textuelle de GCP. Deuxièmement, je propose le cadre fclouds pour assurer une interopérabilité sémantique entre plusieurs nuages, i.e., pour identifier les concepts communs entre les APIs et raisonner dessus. Le langage fclouds est une formalisation des concepts et de la sémantique opérationnelle d’OCCI en employant le langage de spécification formel Alloy. Pour démontrer l’efficacité du langage fclouds, je spécifie formellement treize APIs et en vérifie les propriétés.


Résumé (anglais) : With the advent of cloud computing, different cloud providers with heterogeneous cloud services and Application Programming Interfaces (APIs) have emerged. This heterogeneity complicates the implementation of an interoperable multi-cloud system. Among the multi-cloud interoperability 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 are not 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. I provide two major contributions implemented in the context of the OCCIware project. 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 that is automatically inferred from GCP textual documentation. Second, I propose 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.


Cité Scientifique BP 30155 59653 VILLENEUVE D'ASCQ CEDEX Tél.:+33 (0)3 20 43 44 10