Interprétation Abstraite d’annotations ACSL
Frama-C est un ensemble d’outils pour l’analyse de logiciels C. Dans Frama-C, différentes techniques d’analyse peuvent être implémentées comme plug-ins (greffons) dans un même cadre. La collaboration entre plug-ins repose en partie sur le langage commun de spécification ACSL. Chaque plug-in est supposé interpréter ACSL au mieux de ses possibilités.
Ce post-doctorat consiste à améliorer la précision de l’analyse de valeurs, basée sur la technique d’Interprétation Abstraite, de Frama-C, pour les constructions qui ne sont pas actuellement traitées. Le traitement de certaines constructions nécessitera la conception d’un ou plusieurs domaines abstraits spécifiques.
http://frama-c.com
http://frama-c.com/value.html
http://frama-c.com/acsl.html
Monitoring global pour éoliennes offshore par méthodes de mesure bas coût et à déploiement simplifié
Ce projet fait suite à des travaux antérieurs focalisés sur l’instrumentation d’une éolienne on-shore avec un réseau de capteurs inertiel dont les réponses permettent la détection de modes de vibration propres à l’éolienne, en particulier du mat ainsi que le suivi en temps réel de ces réponses.
Les objectifs de ce projet sont multiples : porter ces travaux sur des éoliennes offshore; rechercher les signatures dans des bandes de fréquences plus larges; étudier la réponse des bases offshore et de leurs ancrages.
L’un des enjeux est notamment de parvenir à retrouver les signatures des éléments tournants (pales) sans instrumentation directe. Instrumenter ces éléments est en effet plus coûteux et plus impactant sur la structure.
En outre la technologie de capteurs sera adaptée au suivi du cycle de vie en fatigue des structures filaires en mouvement (câble de raccordement électrique dynamique et ancrage) dans le cas d’une éolienne off-shore. L’objectif final vise à proposer une méthode globale de suivi de la santé d’une éolienne off-shore.
Post-doc : réseau de neurones CNN - gestion des incertitudes dans la base de données d'apprentissage
L'objectif de ce postdoc est de développer un algorithme pour prendre en compte les incertitudes des données de la base d'apprentissage d'un réseau de neurones. Ce travail s'inscrit dans le contexte d'un projet d'estimation dynamique de l'état d'un procédé d'extraction liquide-liquide. En utilisant un simulateur qualifié du procédé et des mesures de suivi lors de son exploitation, il est possible d'estimer les paramètres opératoires et connaitre ainsi l'état du procédé. Cependant ces mesures sont entachées d'incertitudes et il est nécessaire de réconcilier les données pour obtenir le meilleur jeu de données à fournir au simulateur. Un réseau de neurone convolutifs (CNN) permettant d'inverser le simulateur est en développement (à partir des sorties mesurées, on peut être capable d'estimer les entrées à fournir au simulateur). L'objectif est d'évaluer l'impact des incertitudes de mesure sur la construction de ce réseau de neurones. La première étape sera de propager les incertitudes des mesures d'entrée à travers le simulateur à l'aide de la plateforme Uranie, développée par le CEA ISAS. Cette connaissance sera alors intégrée dans la boucle d'apprentissage du réseau de neurones. L'impact de ces incertitudes sur les résultats du réseau de neurones doit être évalué pour fiabiliser l'estimation de l'état du procédé par le réseau de neurones. A travers ce projet, nous sommes au cœur de la thématique du contrôle de procédés complexes par la simulation.
Conception d’un hyperviseur sûr et sécurisé dans le contexte d’une architecture manycore
Le projet TSUNAMY a pour objectif de re-penser la conception des futures puces manycore selon une approche collaborative matériel/logiciel. Il visera notamment l’intégration de crypto-processeurs dans une telle puce, qui devient du même coup une architecture hétérogène dans laquelle l’ordonnancement, l’allocation, le partage et l’isolation des ressources seront des problématiques majeures.
Le laboratoire LaSTRE a conçu Anaxagoros, un micro-noyau qui assure de bonnes propriétés en termes de sécurité et d’intégration d’applications à criticités mixtes et se prête donc bien à la virtualisation de systèmes d’exploitation. Faire évoluer cette couche de virtualisation dans le cadre du projet TSUNAMY est le principal but de ce sujet de post-doctorat.
Le premier problème à traiter tient au passage d’Anaxagoros à l’échelle des manycores. Ce système a été développé pour s’adapter aux multi-coeurs : des techniques innovantes pour minimiser le nombre de points de synchronisation ont été proposées pour atteindre un haut niveau de parallélisme en mode "lock-free". C’est une première étape, mais le passage aux manycores apporte d’autres problématiques comme la cohérence des caches ou un accès non uniforme à la mémoire, qui nécessitent de se concentrer sur la localité des données. Le second problème sera d’incorporer dans Anaxagoros de véritables capacités de sécurité, notamment dans la protection contre les canaux cachés ou pour la confidentialité. Le troisième et dernier problème qui sera traité par des interactions avec les partenaires du projet sera de déterminer des techniques qui pourront être implémentées directement au niveau matériel pour empêcher que même une faille dans du logiciel habituellement considéré comme sûr ne permettra pas à un attaquant d’obtenir un accès à des données privées ou des fuites d’information.
Gestion Système Multi-Agent optimale des réseaux de chaleur intégrant du stockage thermique
Le travail proposé vise à contribuer au développement des premières briques d’une plate-forme logicielle basée sur les environnements Modelica/JADE (java) permettant de modéliser, simuler et optimiser le pilotage des réseaux de chaleur grâce à l’utilisation de modèles de stockages thermiques compatibles: spécifier les interfaces des données nécessaires et suffisantes pour le contrôle des stocks du réseau, implémenter les éléments contrôlés dans le réseau de chaleur, de définir des modèles simplifiés des principaux composants du réseau de chaleur à intégrer dans les agents(production, distribution/stockage, consommation), et de concevoir des modèles prédictifs de consommation et de production afin de pouvoir anticiper l’évolution du système. L’évaluation des performances se fera sur le cas test construit dans l’environnement de simulation Modelica.
Reconnaissance visuelle à large échelle
Le sujet de ce post-doc concerne la détection et la reconnaissance d’objets dans des images et les flux vidéo à grande échelle. Il s’agit d’une tâche fondamentale qui est l’objet de recherches très actives au niveau mondial, et une tendance affirmée en ce qui concerne les campagnes d’évaluation. L’aspect « grande échelle » concerne à la fois des bases de taille importantes (e.g dix millions d’images) ou un grand nombre de concepts à reconnaître (e.g 100 à 10000). Il s’agit alors de travailler à la fois sur la partie description des images et classification grande échelle.
Au niveau de la description, les résultats de l’état de l’art reposent sur des descripteurs locaux agrégés selon des dictionnaires de « mots visuels »éventuellement construits au moyen de noyaux de Fisher. Il est néanmoins nécessaire de recoder efficacement ces signatures de manière à gérer les grandes bases. Concernant l’apprentissage des concepts visuels ou des objets, de nombreux algorithmes utilisent des séparateurs à vaste marge mais d’autres approches sont parfois envisagées, comme celles basées ou la régression logistique.
Le poste proposé porte sur la recherche et le développement d’algorithmes efficaces permettant de rechercher des entités visuelles dans de très grandes bases. Différentes pistes sont envisagées et devront être discutées avec le candidat sélectionné en fonction des ses connaissances antérieures et de discussions techniques.
Déploiement de protocoles de consensus distribué sur des blockchains de type Smart Contract
L’objectif est de mettre en œuvre divers protocoles de consensus distribué sur des plateformes blockchain de type Smart Contracts aussi bien publiques que privées. Les techniques à la base des preuves d’enjeu et de la gestion de token seront analysées et leur niveau de sécurité sera évalué au regard de la consommation énergétique et de la qualité de la distribution de la confiance dans le système. Les techniques de vérification des transactions de la blockchain Ethereum seront mise en œuvre, ainsi que d’autres algorithmes, plus légers et moins consommateurs d’énergie, dédiés à des blockchains "privées" où les utilisateurs sont authentifiés. La plateforme Hyperledger sera utilisée pour tester les différents protocoles de consensus distribués. De nouveaux algorithmes seront proposés et les solutions retenues seront déployées pour des applications du domaine de l’internet des objets.
Chercheur en intelligence artificielle appliquée à la microfluidique autonome
Cette offre de postdoctorat fait partie du projet 2FAST (Fédération de Laboratoires Fluidiques Autonomes pour Accélérer la Conception de Matériaux) du PEPR DIADEM, qui vise à automatiser complètement la synthèse et la caractérisation en ligne de matériaux à l’aide de puces microfluidiques « orchestrées ». Ces techniques offrent un contrôle précis et tirent parti des avancées numériques pour améliorer les résultats de la chimie des matériaux. Cependant, la caractérisation complète des nano/micro-matériaux à cette échelle reste un défi en raison de son coût et de sa complexité. 2FAST ambitionne d’exploiter les progrès récents dans l'automatisation et de l'instrumentation des plateformes microfluidiques, afin de développer des puces microfluidiques interopérables et automatiquement pilotées permettant une synthèse contrôlée de nanomatériaux. Plus précisément, l'objectif est d'établir une preuve de concept pour une plateforme de réacteur microfluidique/millifluidique à haut débit pour la production continue de nanoparticules de métaux nobles. Des boucles de rétroaction gérées par des outils d’intelligence artificielle contrôleront la progression de la réaction à partir d’informations acquises en ligne par des techniques spectrométriques (UV-Vis, SAXS, Raman). Le postdoctorat proposé porte sur l’ensemble des travaux en intelligence artificielle associés à ces développements, à savoir : i) la conception de boucles de rétroaction, ii) la création d'une base de données de signaux adaptés à l'apprentissage automatique, iii) la mise en œuvre de méthodes d'apprentissage automatique pour connecter les différentes données et/ou piloter les dispositifs microfluidiques autonomes.
Calculs d'évolution à grande échelle avec code Monte-Carlo de transport de neutrons
L'un des principaux objectifs de la physique des réacteurs modernes est d'effectuer des simulations multi-physiques fidèles du comportement d'un cœur de réacteur nucléaire, avec une description détaillée de la géométrie à l'échelle des crayons de combustible. Les calculs multi-physiques en conditions nominales impliquent un couplage entre un solveur de transport pour les neutrons et les précurseurs, des solveurs thermiques et thermohydrauliques pour le transfert de chaleur, et un solveur Bateman pour calculer l'évolution isotopique du combustible nucléaire au cours d'un cycle du réacteur. L'objectif de ce post-doc est de réaliser un tel calcul entièrement couplé, à l'aide de PATMOS, une mini-app Monte-Carlo pour le transport de neutrons, et de la plateforme de couplage C3PO, toutes deux développées au CEA. Le système cible est un cœur de la taille d'un réacteur commercial.
Détection d’attaques dans l’infrastructure de contrôle distribué du réseau électrique
Afin de permettre l’émergence de réseaux d’énergie flexibles et résilients, il faut trouver des solutions aux défis auxquels ils font face. Dans le cadre de ce postdoc on s’intéresse en particulier à la numérisation et la protection des flux de données que cela entraînera, ainsi qu’aux problématiques de cybersécurité.
Dans le cadre du projet Tasting, et en collaboration avec RTE, l’opérateur français du réseau de transport de l’électricité, votre rôle sera de se pencher sur la protection des données de toutes les parties concernées. Le but est de vérifier des propriétés de sécurité sur les données dans des systèmes distribués, qui induisent un certain nombre d’incertitudes par construction.
Pour cela, vous élaborerez une méthodologie outillée pour la protection des données des acteurs du réseau électrique. L'approche sera basée sur les méthodes formelles de vérification à l'exécution appliquées à un système de contrôle distribué.
Cette offre de postdoc s'inscrit dans le cadre du projet TASTING qui vise à relever les principaux défis liés à la modernisation et à la sécurisation des systèmes électriques. Ce projet de 4 ans qui a commencé en 2023 adresse l’axe 3 de l'appel PEPR TASE "Solutions technologiques pour la numérisation des systèmes énergétiques intelligents", co-piloté par le CEA et le CNRS. Les défis scientifiques ciblés concernent l'infrastructure TIC, considérée comme un élément clé et un fournisseur de solutions pour les transformations profondes que nos infrastructures énergétiques subiront dans les décennies à venir.
Dans ce projet sont impliqués deux organismes nationaux de recherche, INRIA et le CEA au travers de son institut de recherche technologique de la direction de la recherche technologique CEA-List. Sont également impliqués 7 laboratoires académiques : le G2Elab, le GeePs, l’IRIT, le L2EP, le L2S et le SATIE, ainsi qu’un partenaire industriel, RTE, qui fournit différents use cases.