Direction scientifique
Transfert de connaissances vers l'industrie

Nos Thèses par thème

Toutes les offres [+]

Vérification hors-ligne d'assertions à l'exécution

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

Master en informatique avec cours de méthodes formelles

SL-DRT-22-0132

Julien.Signoles@cea.fr

Data intelligence dont Intelligence Artificielle (.pdf)

Notre équipe développe Frama-C (http://frama-c.com), une plateforme d'analyse de code C qui fournit plusieurs analyseurs de code. Frama-C est développé en OCaml. Il permet d'annoter des programmes C avec des spécifications formelles écrites dans le langage ACSL. Frama-C peut ainsi garantir qu'un programme C satisfait ses spécifications en se fondant sur des techniques formelles. E-ACSL est l'analyseur de Frama-C dédié à la vérification d'assertions à l'exécution. Il convertit un programme C étendu avec des annotations ACSL en un autre programme C vérifiant la validité des annotations pendant son exécution: par défaut, le programme s'arrête dès qu'une annotation est violée ou, sinon, il se comporte comme le programme original. Pour ce faire, E-ACSL repose sur une instrumentation invasive du code source original afin d'insérer du code qui surveille la validité des annotations ACSL. Cette technique, appellée vérification à l'exécution en-ligne, peut néanmoins s'avérer trop couteuse en temps et en consommation mémoire dans certains contextes d'utilisation. Elle peut aussi soulever des problèmes de sécurité. Le but de la thèse consiste à définir et à implémenter une version hors-ligne d'E-ACSL, compatible avec la version en-ligne existante. La vérification à l'exécution hors-ligne consiste à placer le moniteur dans une entité externe (par exemple, un autre processus sur la même machine ou sur un serveur distant) pour limiter l'instrumentation du code d'origine aux communications avec le moniteur à distance. Cette technique est bien connue et souvent appliquée pour la vérification dynamique de propriétés temporelles, mais elle n'a jamais été appliquée à la vérification d'assertions, qui soulève des problèmes spécifiques liés aux types des données qui doivent être manipulés.

Télécharger l'offre (.zip)

Attestation d'un temps écoulé en embarqué

Département Systèmes (LETI)

Laboratoire Sécurité des Objets et des Systèmes Physiques

M2 sécurité des systèmes embarqués

01-09-2022

SL-DRT-22-0158

christine.hennebert@cea.fr

Cybersécurité : hardware et software (.pdf)

Les objectifs de sécurité des objets connectés sont usuellement la Confidentialité, l'Intégrité et l'Authentification (CIA). Pourtant la garantie de ces objectifs n'empêche pas de changer l'ordonnancement des événements ou la durée séparant deux événements. Pour combler ces nouveaux besoins de sécurité et assurer la sécurité d'un historique de données ou de transactions, les objets connectés doivent être en mesure d'apporter la preuve de l'intervalle de temps séparant deux événements, ou deux blocs de données structurées, au sein d'un système de communication asynchrone. Ce sujet de thèse propose d'explorer de possibles solutions permettant à un dispositif contraint ou IoT de prouver le temps écoulé en se basant sur des composants matériels de sécurité de type TEE (Trusted Execution Environment), SE (Secure Element) et TPM (Trusted Platform Module).

Télécharger l'offre (.zip)

Réseaux de capteurs et Jumeaux numériques pour la Co-conception de systèmes mécatroniques

Département Systèmes (LETI)

Laboratoire Autonomie et Intégration des Capteurs

Ecoles d'ingénieurs / Master 2 en électronique et physique avec des connaissances en simulations électroniques, architectures électroniques et en modélisations et simulations de systèmes multi-physiques (COMSOL, Altair).

01-09-2022

SL-DRT-22-0201

elise.saoutieff@cea.fr

Usine du futur dont robotique et contrôle non destructif (.pdf)

Dans le cadre du développement de ses activités de R&D sur les réseaux de capteurs et les jumeaux numériques (Digital Twins), le Laboratoire Autonomie et Intégration de Capteurs (DSYS/SSCE/LAIC) du CEA-LETI à Grenoble, propose une thèse sur les « Réseaux de capteurs et Jumeaux numériques pour la Co-conception de systèmes mécatroniques ». Le laboratoire LAIC est spécialisé dans la conception et le développement de systèmes électroniques innovants, s'intéressant aux problématiques physiques et électroniques d'interfaces capteurs, d'intégration de capteurs, de basse consommation et de communications avec ou sans fil, pour différents types d'applications dont l'industrie 4.0, l'aéronautique, les dispositifs médicaux, ou encore le sport. L'objet de la thèse sera de mettre en ?uvre un réseau de capteurs combiné à des outils de simulations par éléments finis, puis à des outils d'analyse à base d'Intelligence Artificielle pour développer des Jumeaux Numériques. L'application envisagée est celle des orthèses et prothèses instrumentées pour la médecine du futur, en vue d'améliorer leurs fonctions, leur durée de vie, leur utilité et leur confort pour les utilisateurs dans les phases de rééducation et post-rééducation. Le jumeau numérique sera la réplique virtuelle du système réel en fonctionnement. Il traitera, en temps réel, des informations issues à la fois du réseau de capteurs déployé sur le système (contraintes/déformations, IMU,?) et des modèles de simulations par éléments finis. Il sera utilisé pour évaluer l'état de fonctionnement du système, et notamment son état de vieillissement, mais également pour en prévoir le comportement futur. Ces développements permettront par la suite d'optimiser le fonctionnement, la durée de vie et l'impact environnemental des systèmes mécatroniques (maintenance prédictive, écoconception).

Télécharger l'offre (.zip)

Culture de microalgues sur fumées industrielles

DSUD (CTReg)

Autre DPACA

01-09-2022

SL-DRT-22-0225

florian.delrue@cea.fr

Energie verte et/ou décarbonnée dont bioprocédés et valorisation des déchets (.pdf)

Les microalgues et les cyanobactéries photosynthétiques présentent l'intérêt de pouvoir transformer le CO2 en biomasse valorisable via la photosynthèse. Elles sont potentiellement capables de capter et de réutiliser les émissions de CO2 industrielles et de fait d'atténuer leur impact environnemental. Cette utilisation de CO2 d'origine industrielle dans une logique de bioremédiation de GES est une étape indispensable pour que l'industrie des microalgues puisse passer d'une industrie de spécialités (cosmétique, nutraceutiques) vers une industrie de commodités (énergie, matériaux plastiques, voire protéines animales). Cependant, l'utilisation de CO2 d'origine industrielle par des microorganismes photosynthétiques présente des difficultés d'ordre biologique, chimique et technique. En effet, des questions se posent sur la capacité des microalgues à tolérer ces gaz, sur l'effet de ces gaz sur le pH et la composition des milieux de culture et sur la stratégie à mettre en ?uvre pour optimiser la bioremédiation de ces fumées par les microalgues. Ces études s'effectueront à l'aide du banc expérimental ABIME permettant la culture de microalgues sur des fumées industrielles simulées. Ce projet de thèse se propose d'étudier les verrous biologiques, chimiques et technologiques en jeu lors de la culture de microalgues (et par extension de cyanobactéries photosynthétiques) sur des fumées industrielles, afin de mieux cerner les leviers de changement d'échelle envisageables pour évoluer vers un modèle de production à bas coût et en grande quantité.

Télécharger l'offre (.zip)

Techniques de focalisation en champ proche dans les milieux inhomogènes aux fréquences millimétriques

Département Systèmes (LETI)

Laboratoire Antennes, Propagation, Couplage Inductif

Master electrical engineering / hyperfréquences

01-09-2022

SL-DRT-22-0226

antonio.clemente@cea.fr

Réseaux de communication, internet des objets, radiofréquences et antennes (.pdf)

Dans des multiples applications telles que le transfert d'énergie sans fil, l'imagerie micro-ondes, le contrôle industriel, etc., il est nécessaire de former, diriger ou encore focaliser le rayonnement électromagnétique dans une région spécifique de l'espace. Cette région peut se situer dans l'environnement proche de la surface rayonnante qui a généré l'onde électromagnétique. Dans ce cas, on parle de système focalisant en champ proche. Avec le développement des futurs systèmes de communication de type « Beyond 5G » et 6G, la nécessité de focaliser le faisceau en champ proche peut aussi s'appliquer dans le cas des surfaces intelligentes reconfigurables. Ces dispositifs, si dotés d'éléments reconfigurables, peuvent être utilisés pour manipuler les ondes électromagnétiques et contrôler de manière dynamique les propriétés du canal de propagation. Enfin, la focalisation en champ proche peut aussi être un élément différentiant pour le développement des futurs systèmes d'imagerie médicale qui nécessitent de former et diriger l'énergie dans corps humain afin de diagnostiquer, suivre et / ou soigner des pathologies spécifiques. Dans ce contexte, la focalisation en champ proche peut être utilisée pour améliorer la résolution du système d'imagerie en optimisant le transfert / transmission d'énergie. Le premier objectif de cette thèse est de développer des outils de synthèse, de conception et d'optimisation de systèmes focalisants en champ proche en milieux non homogènes. Ces techniques seront développées en considérant les propriétés électromagnétiques des milieux. La synthèse du champ d'ouverture se fera à partir de l'expansion modale du champ et de la théorie des potentiels vecteurs. Après cette phase, les procédures de synthèse et d'optimisation développées seront utilisées pour concevoir un système focalisant en champ proche opérant aux fréquences millimétriques et / ou sub-THz (30 ? 300 GHz). Ces antennes seront fabriquées et caractérisées en chambre anéchoïque. Des simulations système et / ou des mesures seront aussi faite pour analyser l'impact du système focalisant en champ proche.

Télécharger l'offre (.zip)

5 (Page 1 sur 1)
1
-->

Voir toutes nos offres