Telco Cloud Résilient grâce à la Vérification Continue face aux Comportements Conflictuels // Resilient Telco Cloud through Continuous Verification Tackling Conflicting Behaviors
|
ABG-139077
ADUM-75069 |
Sujet de Thèse | |
| 12/05/2026 | Cifre |
Université de Lille
Villeneuve d'Ascq Cedex - Les Hauts de France - France
Telco Cloud Résilient grâce à la Vérification Continue face aux Comportements Conflictuels // Resilient Telco Cloud through Continuous Verification Tackling Conflicting Behaviors
- Informatique
Cloud Computing, Kubernetes, Cloud native Network Functions, Vérification
Cloud Computing, Kubernetes, Cloud native Network Functions, Verification
Cloud Computing, Kubernetes, Cloud native Network Functions, Verification
Description du sujet
Les industries de télécom connaissent un écosystème mouvant et des transformations technologiques majeures. Elles doivent fiabiliser leurs infrastructures, leurs applications Telco Cloud et anticiper les évolutions rapides des usages et du trafic sur le réseau. Face à des risques de pannes d'envergure, l'exigence de résilience est forte. Elle requiert des mises à jour logicielles fréquentes et la maîtrise de la complexité inhérente de ces systèmes distribués et dynamiques. Les opérateurs Kubernetes sont devenus des contrôleurs logiciels clés pour la gestion du cycle de vie du Telco Cloud. Malgré l'existence de kits de conception et de guides de bonnes pratiques, la diversité des implémentations et les spécificités métiers de ces opérateurs laissent place à des bugs internes, reconnus difficiles à détecter [1]. Les causes sont multiples : configurations incorrectes des ressources manipulées par ces opérateurs, défauts d'ordonnancement des étapes nécessaires au cycle de vie, concurrence entre opérateurs sur une même ressource. Les conséquences prennent différentes formes : panne, blocage, faille de sécurité, perte de données, consommation inutile de ressources [1]. Dans un contexte GitOps et CI/CD, elles concernent toutes les phases du cycle de vie des ressources déployées dans le Cloud. Le fonctionnement des opérateurs Kubernetes, stable, reproductible et sécurisé est donc crucial.
Des travaux académiques récents proposent de générer automatiquement des plans de test [2, 4] ou de la vérification formelle [3] du comportement d'un opérateur avant déploiement. Ces approches se limitent à l'analyse d'un unique opérateur Kubernetes. Elles ne couvrent pas les interactions complexes entre opérateurs, qui provoquent des situations de conflits ou de dépendances critiques, difficiles à déceler lors des phases de réconciliation. Le déploiement de ressources par un opérateur est compromis s'il reste en attente de ressources supprimées ou bloquées par un autre opérateur.
L'objectif de la thèse est de développer des techniques de vérification continue du comportement des opérateurs, fondées sur de l'analyse statique automatisée de leur code en intégrant leurs interactions et l'état réel des ressources déployées. Il s'agit par exemple de vérifier le risque de concurrence entre opérateurs sur une même ressource. L'approche doit répondre aux exigences de déploiement multi-clusters, à grande échelle, d'expressivité des propriétés à garantir et conduire au développement d'outillages intégrables dans des processus CI/CD.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
The telecom industries are experiencing a changing ecosystem and major technological
transformations. They must make their infrastructure and Telco Cloud applications more reliable
and anticipate rapid changes in usage and network traffic.
Confronted with the threat of significant system outages, the requirement for resilience is strong.
It requires frequent software updates and mastering the inherent complexity of these distributed
and dynamic systems. Kubernetes operators have become key software controllers for Telco
Cloud lifecycle management. Despite the existence of design kits and best practice guides, the
diversity of implementations and the business specificities of these operators leave room for
internal bugs, recognized as difficult to detect [1]. The causes are multiple: incorrect
configurations of resources handled by these operators, scheduling defects in the steps
necessary for the lifecycle, race between operators on the same resource. The consequences
take different forms: failure, blocking, security breach, data loss, unnecessary consumption of
resources [1]. In a GitOps and CI/CD context, they concern all phases of the lifecycle of resources
deployed in the Cloud. The operation of Kubernetes operators, stable, reproducible, and secure,
is therefore crucial.
Recent academic works propose to automatically generate test plans [2, 4] or formal verification
[3] of an operator behavior before deployment. These approaches are limited to the analysis of a
single Kubernetes operator. They do not address the complex interactions between operators,
which cause situations of conflict or critical dependencies, difficult to detect during the
reconciliation phases. The deployment of resources by one operator is compromised if it remains
waiting for resources deleted or blocked by another operator.
The objective of the thesis is to develop techniques for continuous verification of operators
behavior, based on automated static analysis of their code by integrating their interactions and
the real state of deployed resources. For instance, it is a matter of checking the risk of competition
between operators on the same resource. The approach must meet the requirements of large-
scale multi-cluster deployments, expressivity of properties to be guaranteed and lead to the
development of tools that can be integrated into CI/CD processes.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
Début de la thèse : 01/10/2026
Des travaux académiques récents proposent de générer automatiquement des plans de test [2, 4] ou de la vérification formelle [3] du comportement d'un opérateur avant déploiement. Ces approches se limitent à l'analyse d'un unique opérateur Kubernetes. Elles ne couvrent pas les interactions complexes entre opérateurs, qui provoquent des situations de conflits ou de dépendances critiques, difficiles à déceler lors des phases de réconciliation. Le déploiement de ressources par un opérateur est compromis s'il reste en attente de ressources supprimées ou bloquées par un autre opérateur.
L'objectif de la thèse est de développer des techniques de vérification continue du comportement des opérateurs, fondées sur de l'analyse statique automatisée de leur code en intégrant leurs interactions et l'état réel des ressources déployées. Il s'agit par exemple de vérifier le risque de concurrence entre opérateurs sur une même ressource. L'approche doit répondre aux exigences de déploiement multi-clusters, à grande échelle, d'expressivité des propriétés à garantir et conduire au développement d'outillages intégrables dans des processus CI/CD.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
The telecom industries are experiencing a changing ecosystem and major technological
transformations. They must make their infrastructure and Telco Cloud applications more reliable
and anticipate rapid changes in usage and network traffic.
Confronted with the threat of significant system outages, the requirement for resilience is strong.
It requires frequent software updates and mastering the inherent complexity of these distributed
and dynamic systems. Kubernetes operators have become key software controllers for Telco
Cloud lifecycle management. Despite the existence of design kits and best practice guides, the
diversity of implementations and the business specificities of these operators leave room for
internal bugs, recognized as difficult to detect [1]. The causes are multiple: incorrect
configurations of resources handled by these operators, scheduling defects in the steps
necessary for the lifecycle, race between operators on the same resource. The consequences
take different forms: failure, blocking, security breach, data loss, unnecessary consumption of
resources [1]. In a GitOps and CI/CD context, they concern all phases of the lifecycle of resources
deployed in the Cloud. The operation of Kubernetes operators, stable, reproducible, and secure,
is therefore crucial.
Recent academic works propose to automatically generate test plans [2, 4] or formal verification
[3] of an operator behavior before deployment. These approaches are limited to the analysis of a
single Kubernetes operator. They do not address the complex interactions between operators,
which cause situations of conflict or critical dependencies, difficult to detect during the
reconciliation phases. The deployment of resources by one operator is compromised if it remains
waiting for resources deleted or blocked by another operator.
The objective of the thesis is to develop techniques for continuous verification of operators
behavior, based on automated static analysis of their code by integrating their interactions and
the real state of deployed resources. For instance, it is a matter of checking the risk of competition
between operators on the same resource. The approach must meet the requirements of large-
scale multi-cluster deployments, expressivity of properties to be guaranteed and lead to the
development of tools that can be integrated into CI/CD processes.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
Début de la thèse : 01/10/2026
Nature du financement
Cifre
Précisions sur le financement
CIFRE ANRT
Présentation établissement et labo d'accueil
Université de Lille
Etablissement délivrant le doctorat
Université de Lille
Ecole doctorale
631 MADIS Mathématiques, sciences du numérique et de leurs interactions
Profil du candidat
Vous êtes diplômé.e d'une école d'ingénieur ou universitaire et titulaire d'un Master Recherche dans le domaine des théories des langages en informatique, des mathématiques appliquées à l'informatique, des sciences et technologies du logiciel, des applications réparties ou des systèmes distribués.
Des compétences en langages de programmation, sémantique, modélisation et vérification formelles sont recherchées pour le poste. En outre, vous présentez une appétence pour le développement d'outils, la validation expérimentale sur plate-forme. Des compétences en Golang, Rust et/ou Python, Linux seront utiles.
Vous disposez également d'une aisance tant à l'oral qu'à l'écrit en français et en anglais, êtes curieux.se, méthodique, autonome, motivé.e par la recherche en milieu industriel, avez un esprit de synthèse, êtes capable de vous intégrer à une équipe de recherche et de travailler en mode collaboratif.
Une première expérience en modélisation d'architecture logicielle répartie, en virtualisation d'infrastructure réseau ou avec les opérateurs Kubernetes serait un plus. Une contribution à la soumission d'un article scientifique serait également fortement appréciée.
You hold an engineering degree or a Master degree in the field of language theories in computer science, mathematics applied to computing, software sciences and technologies, distributed applications or distributed systems. Skills in programming languages, semantics, formal modeling and verification are sought for. Moreover, you have a knack for developing tools and platform experimental validation. Skills in Golang, Rust and/or Python, Linux will be useful. You have a good oral and written level in French and English. You are curious, methodical, autonomous, motivated by research in an industrial environment, have a spirit of synthesis. You are keen to progress in an industrial ecosystem and collaborate with your team. A first experience in distributed software architectures modelling, in virtual network infrastructures or with Kubernetes operators would be a plus. A contribution in a scientific paper would be highly appreciated.
You hold an engineering degree or a Master degree in the field of language theories in computer science, mathematics applied to computing, software sciences and technologies, distributed applications or distributed systems. Skills in programming languages, semantics, formal modeling and verification are sought for. Moreover, you have a knack for developing tools and platform experimental validation. Skills in Golang, Rust and/or Python, Linux will be useful. You have a good oral and written level in French and English. You are curious, methodical, autonomous, motivated by research in an industrial environment, have a spirit of synthesis. You are keen to progress in an industrial ecosystem and collaborate with your team. A first experience in distributed software architectures modelling, in virtual network infrastructures or with Kubernetes operators would be a plus. A contribution in a scientific paper would be highly appreciated.
30/06/2026
Postuler
Fermer
Vous avez déjà un compte ?
Nouvel utilisateur ?
Vous souhaitez recevoir nos infolettres ?
Découvrez nos adhérents
Servier
Nantes Université
Nokia Bell Labs France
Groupe AFNOR - Association française de normalisation
SUEZ
ASNR - Autorité de sûreté nucléaire et de radioprotection - Siège
Institut Sup'biotech de Paris
ONERA - The French Aerospace Lab
Généthon
Aérocentre, Pôle d'excellence régional
TotalEnergies
Tecknowmetrix
Ifremer
Laboratoire National de Métrologie et d'Essais - LNE
ANRT
Medicen Paris Region
ADEME



