Intégration Sécurisée et Évolutive des Logiciels Embarqués dans les Systèmes Interactifs : Approche Formelle dans un Environnement Fog-Cloud

De nos jours, les systèmes interactifs autonomes, tels que les drones et les voitures autonomes, occupent une place centrale dans la transformation technologique actuelle. Leur adoption rapide est motivée par une variété d'applications stratégiques allant de la surveillance et de la sécurité aux livraisons, en passant par le transport autonome et la logistique. Cependant, en raison de la nature critique de ces systèmes, leur sûreté de fonctionnement et leur fiabilité sont des enjeux primordiaux. Ils évoluent dans des environnements souvent imprévisibles et potentiellement dangereux, où la moindre défaillance peut entraîner des conséquences graves, tant en termes de sécurité humaine que matérielle.
Pour cette raison, il est indispensable d'assurer que ces logiciels fonctionnent correctement en toute circonstance. La modélisation formelle permet de représenter mathématiquement le comportement de ces logiciels, garantissant ainsi leur conformité aux spécifications requises. Par ailleurs, la vérification formelle offre des méthodes rigoureuses pour détecter et corriger les erreurs de conception potentielles, augmentant ainsi la fiabilité des systèmes autonomes.
Dans cette perspective, plusieurs travaux de recherche ont déjà exploré l'application de la modélisation et de la vérification formelle dans le contexte des systèmes embarqués et autonomes. Par exemple, l'utilisation de langages de spécification formelle tels que le langage de spécification de système (LTL) a été étudiée pour décrire les propriétés de sûreté et de sûreté de systèmes complexes [1]. De plus, des approches basées sur les réseaux de Petri ont été développées pour modéliser le comportement concurrent et asynchrone des systèmes embarqués, ce qui facilite leur analyse formelle [2].
En ce qui concerne la vérification formelle, des techniques telles que le model checking ont été largement utilisées pour détecter les erreurs de conception et les violations de propriétés spécifiées dans les modèles formels des systèmes [3]. Et, l'utilisation de theorem provers et d'outils de preuve automatique a permis de garantir la correction des logiciels embarqués critiques en vérifiant leur conformité à des spécifications fonctionnelles et de sécurité [4]. Ces approches facilitent l'identification précoce des erreurs, renforçant la robustesse des logiciels embarqués dès les premières phases de développement.
Dans ce contexte, Event-B [5], une méthode formelle basée sur la théorie des événements, a émergé comme un outil puissant pour la modélisation et la vérification formelle des systèmes critiques. L'efficacité d'Event-B a été démontrée dans plusieurs domaines, tels que les systèmes de contrôle industriel et les infrastructures de transport. En spécifiant et en vérifiant le comportement des logiciels embarqués, cette approche permet de garantir la conformité aux exigences fonctionnelles tout en identifiant les incohérences potentielles.
Cependant, l'intégration de ces systèmes interactifs dans des environnements complexes et distribués, tels que ceux utilisant le fog computing [6], soulève de nouveaux défis. Le fog computing, en tant qu'extension du cloud computing vers les périphéries du réseau, distribue les ressources informatiques plus près des appareils embarqués. Cela optimise les délais de traitement, mais nécessite des méthodes avancées pour allouer les ressources de manière efficace tout en maintenant les niveaux de sûreté et de performance requis. De plus, l'introduction de l'intelligence artificielle embarquée ajoute un nouveau niveau de complexité, nécessitant des mécanismes d'explicabilité et de validation afin de garantir l'acceptabilité sociale et la fiabilité des décisions autonomes.
Ainsi, le contexte de cette thèse se situe à l'intersection de plusieurs domaines technologiques majeurs : la modélisation formelle, la vérification des systèmes embarqués, l'optimisation des ressources dans des environnements fog-cloud et l'intégration de l'intelligence artificielle explicable. La convergence de ces technologies est cruciale pour garantir que les systèmes autonomes de demain soient non seulement performants, mais également sûrs et fiables dans des environnements dynamiques et distribués.
Objectifs :
L’objectif principal de cette thèse est de développer un cadre méthodologique pour la modélisation et la vérification formelle des logiciels embarqués dans des systèmes autonomes, tels que les drones et les voitures autonomes, évoluant dans un environnement Fog-Cloud. Cette recherche vise à garantir la fiabilité, la sécurité et l'efficacité de ces systèmes interactifs en s'appuyant sur des méthodes formelles comme Event-B pour spécifier, vérifier et optimiser leur comportement. Ce sujet vise à intégrer les connaissances et les compétences dans le domaine de la modélisation et de la vérification formelle des logiciels embarqués dans les systèmes interactifs tels que les drones et/ou les voitures autonomes. En effet, ces systèmes interactifs sont soumis à des exigences strictes en matière de performance et de sûreté de fonctionnement, notamment dans des environnements dynamiques et potentiellement dangereux.
Nous mettrons donc l'accent sur l'utilisation d'Event-B, une méthode formelle basée sur la théorie des événements, pour la modélisation et la vérification formelle des logiciels embarqués dans les drones et les voitures autonomes.

l’ESME Research Lab est un équipe de recherche à l'ESME et est établie de manière à assurer la cohérence et la continuité des activités de recherche et de formation, tout en prenant en compte les aspects sociétaux et territoriaux. La dimension pluridisciplinaire de l’école nécessite de former une équipe d’enseignantes chercheuses et d’enseignants chercheurs travaillant sur des domaines variés, de la recherche fondamentale en mathématiques à la recherche appliquée en énergie, en électronique ou en technologie de l’information.

Pour mener à bien ses travaux de recherche, l’ESME Research Lab rassemble l’ensemble des permanents impliqués dans des projets de  :

recherche académique, réalisée en partenariat avec des laboratoires universitaires et institutionnels et qui donne lieu à des publications
dans des revues scientifiques et à des communications dans des conférences.

transfert de technologie, consistant en une activité de recherche contractuelle pour le compte d’un partenaire.

recherche partenariale impliquant plusieurs partenaires industriels et institutionnels et dont les retombées peuvent être industrielles comme académiques. »

De formation bac+5, issue d’une école d’ingénieurs ou master avec une spécialisation en informatique, en intelligence artificielle, génie logiciel ou équivalent.
Dynamique, autonome, et organisé.e. Vous faites preuve de créativité, d’esprit d’analyse et de synthèse et vous souhaitez prendre des initiatives et devenir expert. Doté.e d’esprit et d’aisance relationnelle, vous serez en mesure de représenter notre école face à nos parties prenantes.
Bonnes compétences en communication écrite et orale en anglais.
Capacité à organiser et gérer les priorités afin de respecter les délais.
Au cours de vos années de thèse, vous serez tenu de fournir régulièrement des livrables, assurant ainsi un suivi continu de l’avancement de votre recherche.