Intégration Sécurisée et Évolutive des Logiciels Embarqués dans les Systèmes Interactifs : Approche Formelle dans un Environnement Fog-Cloud // Secure and Scalable Integration of Embedded Software in Interactive Systems: A Formal Approach in a Fog-Cloud E

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
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
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

the context of this thesis lies at the intersection of several major technological domains: formal modeling, verification of embedded systems, resource optimization in fog-cloud environments, and the integration of explainable artificial intelligence. The convergence of these technologies is crucial to ensuring that tomorrow's autonomous systems are not only performant but also safe and reliable in dynamic and distributed environments.
The main objective of this thesis is to develop a methodological framework for the formal modeling and verification of embedded software in autonomous systems, such as drones and self-driving cars, operating in a Fog-Cloud environment. This research aims to ensure the reliability, safety, and efficiency of these interactive systems by leveraging formal methods like Event-B to specify, verify, and optimize their behavior.
The aim of this research is to integrate knowledge and skills in the field of formal modeling and verification of embedded software in interactive systems such as drones and/or self-driving cars. Indeed, these interactive systems are subject to strict performance and operational safety requirements, particularly in dynamic and potentially dangerous environments.
Thus, the focus will be on the use of Event-B, a formal method based on event theory, for the formal modeling and verification of embedded software in drones and self-driving cars.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025

Autre type de financement - Autre type de financement,

Université Paris-Saclay GS Informatique et sciences du numérique

580 Sciences et Technologies de l'Information et de la Communication

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.
Master's degree (or equivalent) in computer science, artificial intelligence, software engineering, or a related field. ▪ Dynamic, autonomous, and organized. You possess creativity, analytical thinking, and synthesis skills, and you are eager to take initiative and become an expert. With strong communication and interpersonal skills, you will represent our school in front of stakeholders. ▪ Good writen and communication skills in English. ▪ Ability to organize and manage priorities in order to meet deadline ▪ Throughout your PhD, you will be expected to provide regular deliverables, ensuring continuous monitoring of your research progress.