Intégration Sécurisée Et Évolutive Des

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

- Réf **ABG-126151**
- Sujet de Thèse- 07/10/2024- Autre financement privé- ESME Sudria- Lieu de travail- Ivry sur Seine et Vélizy - Ile-de-France - France- Intitulé du sujet- Intégration Sécurisée et Évolutive des Logiciels Embarqués dans les Systèmes Interactifs : Approche Formelle dans un Environnement Fog-Cloud- Champs scientifiques- Informatique
- Mots clés- Logiciels Embarqués,Systèmes Interactifs, Vérification Formelle, Sécurité, Fog-Cloud**Description du sujet**:
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.
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.

**Nature du financement**:

- Autre financement privé**Précisions sur le financement**:
**Présentation établissement et labo d'accueil*