Scientific direction Development of key enabling technologies
Transfer of knowledge to industry

Programme de stages

Etude de la mise en œuvre d’un environnement de co-émulation générique basé sur FPGA

LIST/DACLE/LCE

Electronique - Electricité - Electronique embarquée

Saclay

Région parisienne (91)

6 mois

Ingénieur/Master

3361156

Les candidatures doivent être adressées par email et sous forme d'un CV et d'une lettre de motivation détaillant les compétences à :
CEA Grenoble

17 rue des martyrs
38054 Grenoble
e-mail : caaliph.andriamisaina@cea.fr

Avec l'augmentation de la complexité des systèmes sur puces (SoC), 70% des efforts de conception sont passés dans la phase de vérification. Cette phase de vérification s'effectue généralement à l'aide de logiciels de simulation tels que Modelsim, VCS, … Cependant, ces logiciels de simulation sont trop lents et ne peuvent pas suivre l'augmentation de la complexité des SoC. L'émulation est une alternative qui a pris de la place dans le flot de vérification offrant des fréquences de simulation largement supérieures aux logiciels de simulation, mais avec des coûts importants. Les émulateurs permettent de simuler des circuits complexes à des fréquences de quelques centaines de KHz voire plus d'1MHz. Ces fréquences restent limitées pour exécuter du logiciel et des milliards de cycle d'opérations logicielles tout en utilisant les interfaces et l'environnement réel des applications futures. Le prototypage rapide sur FPGA est une alternative viable pour répondre aux challenges décrits précédemment car il permet d'atteindre plusieurs MHz de fréquence de simulation. Cependant, le prototypage sur FPGA est limité en visibilité pour permettre une analyse détaillée de l'exécution. Ainsi, la co-émulation, basée sur un couplage entre un simulateur rapide (décrit au niveau transactionnel) s'exécutant sur un PC et une plate-forme FPGA intégrant des moniteurs, permet de pallier à cette limite de visibilité tout en gardant la rapidité de simulation.L'objectif du stage est dans un premier temps, de faire une étude bibliographique et qualitative des différentes méthodes de communication utilisées dans la co-émulation. Cet état de l'art a pour but d'identifier les différentes couches de communication utilisées entre un simulateur et une plate-forme FPGA.La seconde étape consiste à coupler un simulateur décrit en systemC et une plateforme d'évaluation FPGA VC707 de Xilinx. Pour ce couplage, il est nécessaire de développer les couches de communications identifiées lors de l'étude bibliographique. Ce stage permettra au candidat d'approfondir ses compétences en méthodologie de conception des SoC et en développement sur FPGA.

Régularisation d’images d’orientations cristallines utilisées pour la simulation de contrôles ultrasonores de soudures

LIST/DISC/LSMA

Mathématiques - Analyse numérique

Saclay

Région parisienne (91)

Ingénieur/Master

3361150

Les candidatures doivent être adressées par email et sous forme d'un CV et d'une lettre de motivation détaillant les compétences à :
CEA Grenoble

17 rue des martyrs
38054 Grenoble
e-mail : ekaterina.iakovleva@cea.fr

Le CEA LIST mène des activités de recherche et développement dans le domaine du contrôle non destructif (CND) qui consiste à caractériser l'état d'intégrité de structures industrielles sans les dégrader. Parallèlement à la conception de capteurs innovants et au développement de nouvelles méthodes de contrôles, le LIST développe la plate-forme CIVA (http://www-civa.cea.fr) logiciel de simulation de CND qui s'appuie sur les travaux de recherches menés au laboratoire en modélisation RX, électromagnétique et ultrasonore. Des outils de simulation de contrôle non destructif de soudures sont en cours de développement. La soudure pouvant être décrite comme un milieu anisotrope d'orientation cristalline variable, des algorithmes de tracés de rayons en milieux inhomogène sont utilisés. Ils sont basés sur la résolution d'un système différentiel non-linéaire qui permet d'obtenir la trajectoire des rayons. Ces algorithmes prennent comme données d'entrée l'orientation cristalline à n'importe quelle position de la soudure, cette dernière est obtenue par interpolation de type B-spline (bi ou tri)cubique à partir d'une cartographie d'orientations cristallines à 2 ou 3 dimensions respectivement. Cependant, en pratique, ces cartographies peuvent présenter de très fortes variations des orientations cristallines, ce qui les rend incompatibles avec des modèles rayons. L'objectif du stage est de définir une méthode de lissage de la cartographie d'orientations cristallines à 2 et 3 dimensions afin de réduire les irrégularités et singularités présentent dans la description. Cette technique de lissage sera basée sur les fonctions splines lissantes dont le but, à l'origine, est d'approcher un ensemble de points par une fonction continue plutôt que d'interpoler exactement ces points. L'influence de la description de la soudure sera étudiée à travers le nouveau schéma de lissage proposée. Le stage comportera à la fois un volet théorique (bibliographie, collecte, analyse et étude des méthodes de lissage de la description du sous-sol terrestre utilisées en géophysique) et un volet algorithmique et requiert un goût prononcé pour le traitement d'image et analyse numérique. L'étudiant intégrera l'équipe de modélisation du laboratoire et sera encadré par un ingénieur chercheur spécialisé dans le domaine de la simulation ultrasonore. Ce stage d'une durée de 6 mois peut déboucher, le cas échéant, sur une proposition de thèse. Le stagiaire perçoit une gratification mensuelle. Par ailleurs le stagiaire peut bénéficier des facilités de transport du CEA.

Vérification d'un micro­noyau sécurisé d'hyperviseur

DRT/LIST/DILS/LSL

Informatique - Informatique

Saclay

Région parisienne (91)

4-6 mois

Ingénieur/Master

3360473

Les candidatures doivent être adressées par email et sous forme d'un CV et d'une lettre de motivation détaillant les compétences à :
CEA Grenoble

17 rue des martyrs
38054 Grenoble
e-mail : Nikolai.Kosmatov@cea.fr

Cadre Le CEA LIST est un centre de recherche technologique sur les systèmes à logiciel prépondérant qui mène ses recherches en partenariat avec les grands acteurs industriels du nucléaire, de l’automobile, de l’aéronautique, de la défense et du médical pour étudier et développer des solutions innovantes adaptées à leurs besoins. Au sein du CEA LIST, le Laboratoire Sûreté des Logiciels (LSL), localisé à Palaiseau (Essonne), développe les outils d'aide à la validation et à la vérification de logiciels et de systèmes matériels/logiciels. L'un de ces outils, nommé Frama­C, permet de calculer les valeurs possibles des variables à chaque point de programme, trouver des menaces d'erreurs à l'exécution, prouver des propriétés du programme ou les vérifier à l'exécution, générer des cas de test, etc. Un micro­noyau sécurisé pour une solution d'hypervision dite « en aveugle » a été développé par un autre laboratoire du CEA LIST. Il garantit la confidentialité et l’intégrité des données des machines virtuelles. Notamment, l'hyperviseur en aveugle n'a pas accès à la partition mémoire réservée pour une machine virtuelle car seul le micro­noyau sécurisé possède un contrôle total de la mémoire. Objectifs Ce stage vise à vérifier des algorithmes du micro­noyau sécurisé à l'aide des méthodes formelles (preuve de programmes, analyse de valeurs), de vérification à l'exécution et de test structurel en utilisant la plate­forme Frama­C. Un des composants critiques à vérifier est lié à la gestion de la mémoire. Les algorithmes seront spécifiés et prouvés à l'aide des greffons de preuve de Frama­C. Des méthodes complémentaires (test, vérification à l'exécution) seront utilisées pour des fonctions qui ne seront pas entièrement prouvées. Ce stage permettra au stagiaire de découvrir divers outils de vérification de logiciels et les technologies utilisées, les appliquer à la vérification d'un cas d'étude réel, et d'acquérir ainsi des compétences de plus en plus demandées par les entreprises. Il existe des possibilités de continuer en thèse au CEA après le stage. Candidatures Bonnes connaissances en génie logiciel, un goût pour les mathématiques et la logique. Langage C, notions en architecture et systèmes d'exploitation souhaités. Capacité de travail en équipe. Les délais administratifs de recrutement au CEA étant de 2 à 3 mois minimum, merci de prendre contact le plus tôt possible. Encadrement : Nikolay Kosmatov Contact : nikolay.kosmatov@cea.fr Références [1] M, Aichouch and M. Ait Hmid. Towards an Implementation of a Blind Hypervisor. In : SEC2, https://sec2­2015.inria.fr/files/2015/06/aichouch­paper.pdf [2] F.Kirchner, N.Kosmatov, V.Prevosto, J.Signoles, B.Yakobowski: Frama­C ­ A Software Analysis Perspective. Formal Asp. Comput. 27(3): 573­-609 (2015) http://kosmatov.perso.sfr.fr/nikolai/publications/kirchner_kpsy_faoc_2015.pdf

Vérification d'un protocole de communication de réseau de capteurs à l'aide d'outils de vérification automatique

DRT/LIST/DILS/LSL

Informatique - Informatique

Saclay

Région parisienne (91)

4-6 mois

Ingénieur/Master

3360472

Les candidatures doivent être adressées par email et sous forme d'un CV et d'une lettre de motivation détaillant les compétences à :
CEA Grenoble

17 rue des martyrs
38054 Grenoble
e-mail : Nikolai.Kosmatov@cea.fr

Cadre Le CEA LIST est un centre de recherche technologique sur les systèmes à logiciel prépondérant qui mène ses recherches en partenariat avec les grands acteurs industriels du nucléaire, de l’automobile, de l’aéronautique, de la défense et du médical pour étudier et développer des solutions innovantes adaptées à leurs besoins. Au sein du CEA LIST, le Laboratoire de Sûreté des Logiciels (LSL), localisé à Saclay (Essonne), développe les outils d'aide à la validation et à la vérification de logiciels et de systèmes matériels/logiciels. L'un de ces outils, nommé Frama­C, permet de calculer les valeurs possibles des variables à chaque point de programme, trouver des menaces d'erreurs à l'exécution, prouver des propriétés du programme ou les vérifier à l'exécution, générer des cas de test, etc. Dans le cadre d'un projet collaboratif, le CEA LIST travaille sur l'implémentation et la validation de protocoles de réseaux de capteurs qui seront utilisés dans des domaines critiques (avionique, transport, etc.) Objectifs Ce stage vise à vérifier des logiciels embarqués dans un réseau de capteurs à l'aide des outils de vérification automatique. Dans un premier temps, il s'agira d'identifier et de spécifier des propriétés de sûreté et sécurité de fonctionnement, notamment, liées à la communication et diffusion de messages. Ces propriétés seront ensuite spécifiées dans le langage de spécification de la plate­forme Frama­C, incluant des preconditions, postconditions, assertions, etc. Ensuite, des outils de vérification seront appliqués pour vérifier les propriétés spécifiés et identifier des éventuelles erreurs. Les algorithmes seront spécifiés et ensuite prouvés à l'aide des greffons de preuve de Frama­ C. Le prototype développé au CEA LIST sera utilisé comme le point de départ des travaux. Les techniques de test ou vérification à l'exécution pourront être utilisées pour la validation des parties du code qui ne pourront pas être entièrement prouvées. Ce stage permettra au stagiaire de découvrir divers outils de vérification de logiciels et les technologies utilisées pour assurer la sûreté et la sécurité de logiciels, les appliquer à la vérification d'un cas d'étude réel, et d'acquérir ainsi des compétences de plus en plus demandées par les entreprises. Il existe des possibilités de continuer en thèse au CEA après le stage. Candidatures Des connaissances en génie logiciel, un goût pour les mathématiques et la logique. Bonnes connaissances du langage C, notions en protocoles de communication souhaitées. Capacité de travail en équipe. Les délais administratifs de recrutement au CEA étant de 2 à 3 mois minimum, merci de prendre contact le plus tôt possible. Encadrement : Nikolay Kosmatov Contact : nikolay.kosmatov@cea.fr Références : F.Kirchner, N.Kosmatov, V.Prevosto, J.Signoles, B.Yakobowski: Frama­C ­ A Software Analysis Perspective. Formal Asp. Comput. 27(3): 573­-609 (2015) http://kosmatov.perso.sfr.fr/nikolai/publications/kirchner_kpsy_faoc_2015.pdf

Extension d'une bibliothèque de simulation pour le monitoring de la mémoire

DRT/LIST/DILS/LSL

Informatique - Informatique

Saclay

Région parisienne (91)

5-6 mois

Ingénieur/Master

3360471

Les candidatures doivent être adressées par email et sous forme d'un CV et d'une lettre de motivation détaillant les compétences à :
CEA Grenoble

17 rue des martyrs
38054 Grenoble
e-mail : Nikolai.Kosmatov@cea.fr

Cadre Le CEA LIST est un centre de recherche technologique sur les systèmes à logiciel prépondérant qui mène ses recherches en partenariat avec les grands acteurs industriels du nucléaire, de l’automobile, de l’aéronautique, de la défense et du médical pour étudier et développer des solutions innovantes adaptées à leurs besoins. Au sein du CEA LIST, le Laboratoire Sûreté des Logiciels (LSL), localisé à Palaiseau (Essonne), développe les outils d'aide à la validation et à la vérification de logiciels et de systèmes matériels/logiciels. L'un des nos outils, nommé Frama­C (http://frama­c.com), offre différents greffons pour l'analyse et la vérification de code C. Dans Frama­C, un programme C peut être annoté, c'est­à­dire, contenir des propriétés à vérifier exprimées par des annotations dans un langage de spécification formelle. Un des greffons de Frama­C, nommé E­ACSL, permet d'évaluer les annotations lors de l'exécution grâce à une instrumentation de code C, et de rapporter des échecs éventuels. Certaines de ces annotations portent sur des locations mémoires du programme (validité, initialisation, etc.). Un autre outil développé au LSL, UNISIM, offre une bibliothèque de simulation permettant de simuler sur un PC et de surveiller, à la manière des outils de débogage, l'exécution d'un code embarqué. La version actuelle de la bibliothèque ne surveille pas spécifiquement la validité et l'initialisation des blocs mémoires dans l'exécution du programme simulé. Objectifs La version existante du greffon E­ACSL effectue une instrumentation qui rajoute des variables et du code supplémentaires, ce qui n'est pas souhaitable dans un contexte très contraint du code embarqué. Dans le cadre d'un projet de développement d'un nouvel outil de monitoring et d'évaluation des annotations à l’exécution pour le code embarqué, ce stage vise à réaliser une extension de la bibliothèque de simulation d'UNISIM pour le monitoring avancé de la mémoire. La première étape du stage consistera à identifier des moments dans l'exécution simulée et des informations qui doivent être signalées à l'outil de monitoring « à distance » afin de pouvoir mettre à jour le statut de la mémoire (allocation et libération des blocs mémoires, initialisation etc.). Ensuite, il faudra réaliser le transfert de ces informations vers l'outil de monitoring qui devra maintenir un modèle mémoire à jour afin de pouvoir évaluer les annotations sur l'état de la mémoire. Enfin, des expérimentations seront effectuées pour évaluer la solution développée. Ce stage permettra au stagiaire de contribuer à la réalisation d'un outil de simulation et monitoring innovant, de l'évaluer sur des études de cas, et d'acquérir ainsi des compétences en simulation et vérification du code embarqué. Il existe des possibilités de continuer en thèse au CEA après le stage. Candidatures Bonne maîtrise des langages C et C++ et de la programmation bas niveau. Connaissances en débogage et communication entre programmes souhaitées. Capacité de travail en équipe. Les délais administratifs de recrutement au CEA étant de 2 à 3 mois minimum, merci de prendre contact le plus tôt possible. Encadrement : Nikolay Kosmatov, Gilles Mouchard, Julien Silgnoles. Contact : nikolay.kosmatov@cea.fr Référence : M. Delahaye, N. Kosmatov, and J. Signoles. Common specification language for static and dynamic analysis of C programs. In SAC’13, pages 1230–1235, 2013. http://kosmatov.perso.sfr.fr/nikolai/publications/delahaye_ks_sac_2013.pdf

Développement d'un outil de monitoring à base de simulation pour le code embarqué

DRT/LIST/DILS/LSL

Informatique - Informatique

Saclay

Région parisienne (91)

5-6 mois

Ingénieur/Master

3360470

Les candidatures doivent être adressées par email et sous forme d'un CV et d'une lettre de motivation détaillant les compétences à :
CEA Grenoble

17 rue des martyrs
38054 Grenoble
e-mail : Nikolai.Kosmatov@cea.fr

Cadre Le CEA LIST est un centre de recherche technologique sur les systèmes à logiciel prépondérant qui mène ses recherches en partenariat avec les grands acteurs industriels du nucléaire, de l’automobile, de l’aéronautique, de la défense et du médical pour étudier et développer des solutions innovantes adaptées à leurs besoins. Au sein du CEA LIST, le Laboratoire Sûreté des Logiciels (LSL), localisé à Palaiseau (Essonne), développe les outils d'aide à la validation et à la vérification de logiciels et de systèmes matériels/logiciels. L'un des nos outils, nommé Frama­C (http://frama­c.com), offre différents greffons pour l'analyse et la vérification de code C. Dans Frama­C, un programme C peut être annoté, c'est­à­dire, contenir des propriétés à vérifier exprimées par des annotations dans un langage de spécification formelle. Un des greffons de Frama­C, nommé E­ACSL, permet d'évaluer les annotations lors de l'exécution grâce à une instrumentation de code C, et de rapporter des échecs éventuels. Un autre outil développé au LSL, UNISIM, offre une bibliothèque de simulation permettant de simuler sur un PC et de surveiller, à la manière des outils de débogage, l'exécution d'un code embarqué. Objectifs La version existante du greffon E­ACSL effectue une instrumentation du programme C qui rajoute des variables et du code supplémentaires, ce qui n'est pas souhaitable dans un contexte contraint du code embarqué. Ce stage vise à développer un nouvel outil de monitoring et d'évaluation des annotations à l’exécution adapté aux contraintes du code embarqué. Il sera basé sur la simulation du code non­instrumenté à l'aide de la bibliothèque de simulation d'UNISIM. La première étape du stage consistera à concevoir un protocole de communication avec une bibliothèque de simulation afin de pouvoir demander et transmettre les informations nécessaires pour évaluer les annotations (e.g. les valeurs des variables du programme). Ensuite, il faudra développer (en OCAML, dans un greffon de Frama­C) un outil de monitoring « à distance » qui fera des requêtes pour demander des informations nécessaires sur l'exécution simulée en utilisant le protocole défini, et réalisera l'évaluation des annotations. La version existante de E­ACSL pourra servir d'un point de départ pour cette implantation. Enfin, cet outil sera expérimenté sur des exemples de code embarqué. Ce stage permettra au stagiaire de réaliser un outil de monitoring innovant, de l'appliquer à la vérification d'études de cas, et d'acquérir ainsi des compétences en vérification de code embarqué. Il existe des possibilités de continuer en thèse au CEA après le stage. Candidatures Bonne maîtrise des langages OCAML, C/C++. Connaissances en débogage et communication entre programmes souhaitées. Capacité de travail en équipe. Les délais administratifs de recrutement au CEA étant de 2 à 3 mois minimum, merci de prendre contact le plus tôt possible. Encadrement : Nikolay Kosmatov, Gilles Mouchard, Julien Silgnoles. Contact : nikolay.kosmatov@cea.fr Référence : M. Delahaye, N. Kosmatov, and J. Signoles. Common specification language for static and dynamic analysis of C programs. In SAC’13, pages 1230–1235, 2013. http://kosmatov.perso.sfr.fr/nikolai/publications/delahaye_ks_sac_2013.pdf

148 Results found (Page 12 of 25)
first   previous  10 - 11 - 12 - 13 - 14  next   last

Voir toutes nos offres