Qui sommes-nous ?
Espace utilisateur
Formation continue
Credit : L. Godart/CEA
D’un jour à plusieurs semaines, nos formations permettent une montée en compétence dans votre emploi ou accompagnent vers le retour à l’emploi. 
Conseil et accompagnement
Crédit : vgajic
Fort de plus de 60 ans d’expériences, l’INSTN accompagne les entreprises et organismes à différents stades de leurs projets de développement du capital humain.
Thèses
Accueil   /   Thèses   /   Cadre formel pour la spécification et la vérification de flots de communication de processus distribués dans le Cloud

Cadre formel pour la spécification et la vérification de flots de communication de processus distribués dans le Cloud

Défis technologiques Informatique et logiciels Réseaux de communication, internet des objets, radiofréquences et antennes Sciences pour l’ingénieur

Résumé du sujet

Les clouds sont constitués de serveurs interconnectés via internet, sur lesquels on peut implémenter des systèmes faisant usages d’applications et de bases de données déployées sur les serveurs. L’informatique basée sur les clouds gagne considérablement en popularité, y compris pour y déployer des systèmes critiques. De ce fait, disposer d’un cadre formel pour raisonner sur ce type de systèmes devient une nécessité. Une exigence sur un tel cadre est qu’ils permettent de raisonner sur les concepts manipulés dans un cloud, ce qui inclue naturellement la capacité à raisonner sur des systèmes distribués, composés de sous-systèmes déployés sur différentes machines et interagissant par passage de messages pour réaliser des services. Dans ce contexte, la facilité à raisonner sur les flots de communications est un élément central. L'objectif de cette thèse est de définir un cadre formel outillé dédié à la spécification et la vérification de systèmes déployés sur des clouds. Ce cadre capitalisera sur le cadre formel des "interactions". Les interactions sont des modèles dédiés à la spécification des flots de communications entre différents acteurs d'un système. Les travaux de thèse étudieront comment définir des opérateurs de structuration (enrichissement, composition) et de raffinement pour permettre de mettre en œuvre des processus de génie logiciel classique en se basant sur les interactions.

Laboratoire

Département Ingénierie Logiciels et Systèmes (LIST)
LECS (DILS)
Laboratoire exigences et conformité des systèmes
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down