Thèse de Trinh Le Khanh

Conception d'applications cloud auto-adaptatives correctes par construction à l'aide de méthodes formelles

Il est essentiel de coordonner correctement l'accès aux ressources cloud entre les composants logiciels cloud simultanés pour s'assurer qu'ils satisfont aux exigences des utilisateurs et du système et éviter les pannes opérationnelles et les blocages. Les systèmes cloud doivent être capables de s'adapter aux changements au moment de l'exécution sans interruption. Les approches traditionnelles ne séparent pas le code métier des calculs des composants de leur coordination, ce qui rend difficile le débogage et la maintenance. Les changements dans les politiques de coordination nécessitent non seulement de reprogrammer les composants, mais affectent également les autres composants qui interagissent avec eux. Dans ce doctorat thèse, nous ciblons la bonne coordination de l'accès aux ressources cloud entre les entités applicatives cloud concurrentes. Notre objectif est de garantir que les entités d'applications cloud simultanées disposent d'un accès correct aux ressources cloud. Dans cette thèse, j'apporte trois contributions principales: - J'introduis une approche de spécification basée sur une ontologie pour proposer NaturalBIP --- un langage pour spécifier les exigences fonctionnelles. Cette ontologie définit précisément les concepts et leurs relations dans un domaine spécifique. Ensuite, les spécifications sont écrites dans des modèles pseudo-naturels avec des espaces réservés restreints par les concepts de l'ontologie. - Je fournis un compilateur pour analyser et traduire les spécifications écrites en langage NaturalBIP en artefacts JavaBIP (c'est-à-dire JavaBIP GlueBuilder, transferts de données et propriétés de sécurité) et connecteurs BIP. - J'étends OCCIware avec des capacités de coordination à l'aide de JavaBIP. J'utilise la spécification Finite State Machine (FSM) dans la conception OCCIware pour spécifier le comportement du composant. Ensuite, la coordination entre eux est établie par JavaBIP généré à partir du compilateur NaturalBIP. Je calcule également des modèles BIP à partir des connecteurs BIP et du modèle de configuration pour vérifier la propriété sans blocage à l'aide d'iFinder, un outil de détection compositionnelle des blocages au moment de la conception. Avec ces contributions, je propose une chaîne d'outils pour développer des applications cloud auto-adaptatives correctes par construction et conclus cette thèse en présentant des perspectives futures pour améliorer ce travail.

Jury

M. Philippe MERLE Université de Lille Directeur de thèse M. Jean-Marie JACQUET University of Namur Rapporteur M. Marius BOZGA CNRS-VERIMAG Rapporteur M. Simon BLIUDZE Centre Inria de l'Université de Lille Examinateur Mme Olga KOUCHNARENKO University of Franche-Comté Examinatrice

Thèse de l'équipe Spirals soutenue le 27/01/2023