Modélisation des Systèmes Élastiques Cloud : vers la Vérification Formelle de leur Comportement

Résumé

Les dernières années ont vu l'émergence d'un nouveau type de systèmes autonomiques appelés les systèmes élastiques cloud. La caractéristique qui a rendu ces systèmes très populaires dans les secteurs académiques et industriels est leur capacité de gérer et planifier la consommation des ressources pour maintenir une bonne qualité de service (QoS) dans un système cloud, tout en réduisant les coûts de fonctionnement à travers l'utilisation des solutions de contrôle d'élasticité. L'approvisionnement des ressources suffisantes pour le bon fonctionnement d'un système cloud, sans aucun gaspillage n'est pas une tâche triviale. Une bonne solution d'élasticité doit se baser sur un modèle précis et complet qui permet de décrire les architectures des systèmes cloud et leur comportement élastique, tout en capturant les complexités internes. Dans ce contexte, les méthodes formelles caractérisées par leur efficacité, rigueur et précision présentent une solution efficace pour répondre aux exigences de modélisation et d'analyse de ce type de systèmes. L'état de l'art montre qu'aucune des quelques approches formelles actuelles, ne fournit une méthodologie générique et complète qui couvre tous les aspects relatifs à la modélisation et l'analyse des systèmes élastiques basés cloud. La majorité des propositions existantes se focalisent principalement sur le niveau infrastructure du cloud et l'élasticité horizontale sans prendre en considération des aspects structurels. Pour pallier à ce manque, le travail présenté dans cette thèse s'intéresse à la proposition d'une approche générique et exhaustive basée sur un cadre formel permettant de spécifier les architectures des systèmes basés cloud, ainsi que la modélisation et la vérification de leur comportement élastique. En premier lieu, nous adoptons les systèmes réactifs bigraphiques et la logique de typage pour définir un modèle structurel qui permet de décrire les éléments architecturaux dans un système cloud, les relations et les dépendances entre ces éléments et aussi les contraintes structurelles et relationnelles qui en régissent le comportement élastique. Ensuite, nous proposons deux catégories principales de règles de réaction bigraphiques afin de fournir les mécanismes nécessaires pour modéliser tous les aspects comportementaux des systèmes élastiques basés cloud, tout en tenant compte des points de vue client et cloud. Enfin, pour valider l'approche proposée, nous avons développé le prototype MoveElastic, qui est un Framework basé sur un couplage judicieux entre les systèmes réactifs bigraphiques et le langage Maude pour la spécification des architectures des systèmes cloud et la vérification de leurs propriétés d'élasticité.

Citer ce document

Accès au document

Ce document est hébergé sur son dépôt institutionnel d'origine.

Auteur(s)

Statistiques

Consultations : 3

Téléchargements : 0