Informations générales
Entité de rattachement
Le CEA est un acteur majeur de la recherche, au service des citoyens, de l'économie et de l'Etat.
Il apporte des solutions concrètes à leurs besoins dans quatre domaines principaux : transition énergétique, transition numérique, technologies pour la médecine du futur, défense et sécurité sur un socle de recherche fondamentale. Le CEA s'engage depuis plus de 75 ans au service de la souveraineté scientifique, technologique et industrielle de la France et de l'Europe pour un présent et un avenir mieux maîtrisés et plus sûrs.
Implanté au cœur des territoires équipés de très grandes infrastructures de recherche, le CEA dispose d'un large éventail de partenaires académiques et industriels en France, en Europe et à l'international.
Les 20 000 collaboratrices et collaborateurs du CEA partagent trois valeurs fondamentales :
• La conscience des responsabilités
• La coopération
• La curiosité
Référence
SL-DRT-24-0755
Direction
DRT
Description du sujet de thèse
Domaine
Défis technologiques
Sujets de thèse
Cadre formel pour la spécification et la vérification de flots de communication de processus distribués dans le Cloud
Contrat
Thèse
Description de l'offre
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.
Université / école doctorale
Sciences et Technologies de l’Information et de la Communication (STIC)
Ecole Centrale Paris
Localisation du sujet de thèse
Site
Saclay
Critères candidat
Formation recommandée
Méthodes formelles
Demandeur
Disponibilité du poste
01/09/2024
Personne à contacter par le candidat
GASTON Christophe christophe.gaston@cea.fr
CEA
DRT/DILS//LECS
CEA/Saclay
01 69 08 34 82
Tuteur / Responsable de thèse
LEGALL Pascale pascale.legall@ecp.fr
CentraleSupélec
Laboratoire de Mathématiques et Informatique pour la Complexité et les Systèmes (MICS)
CentraleSupélec - Université de Paris-Saclay
9 rue Joliot-Curie, F-91192 Gif-sur-Yvette Cedex
En savoir plus