Thèse Model Checking des Systèmes Ouverts Fondements Logiques et Algorithmes Basés sur les Automates Ouverts H/F - 75

Établissement : Institut Polytechnique de Paris Télécom Paris
École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris
Laboratoire de recherche : Laboratoire de Traitement et Communication de l'Information
Direction de la thèse : Rabea AMEUR-BOULIFA ORCID 0000000224718012
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-04-15T23:59:59Les applications distribuées à grande échelle, fonctionnant sur des infrastructures hétérogènes et élastiques telles que les plateformes cloud, et capables de reconfiguration dynamique ou de comportement autonome, sont de plus en plus courantes dans les systèmes d'entreprise. Leur conception et leur analyse sont sujettes à des erreurs et se révèlent plus complexes que pour les applications traditionnelles.
Cette thèse porte sur le développement de méthodes et d'outils visant à garantir la correction de la composition des composants logiciels ainsi qu'à détecter et prévenir les interblocages, en proposant un cadre systématique et rigoureux pour la vérification de systèmes complexes, ouverts et dynamiques.

Les applications distribuées à grande échelle, déployées sur des infrastructures hétérogènes et élastiques telles que les plateformes cloud, se multiplient dans les systèmes d'entreprise modernes. Ces systèmes sont de plus en plus dynamiques, capables de reconfiguration autonome ou de comportements adaptatifs en fonction de leur environnement.

La conception et l'analyse de ces systèmes posent des défis majeurs : la complexité inhérente, la nature ouverte et dynamique des architectures distribuées, ainsi que les interactions entre composants peuvent générer des erreurs critiques et des blocages (deadlocks). Les approches traditionnelles de vérification et de test sont souvent insuffisantes pour garantir la correction et la fiabilité de tels systèmes.

Cette thèse s'inscrit dans le cadre des recherches en vérification formelle, modélisation de composants logiciels et analyse de systèmes dynamiques. L'objectif scientifique est de développer des méthodes et outils permettant d'assurer la correction de la composition des composants logiciels, de détecter et prévenir les interblocages, et de proposer un cadre systématique et rigoureux pour la vérification des systèmes distribués complexes, ouverts et dynamiques.