X

Job Offers

Ingénieur de recherche « vérification et évaluation d’architectures concurrentes » (F/H)

IRT Saint Exupéry

Département: Systèmes Embarqués

N+1 : Responsable de Pôle

Lieu : Toulouse

L’Institut de Recherche Technologique Antoine de Saint Exupéry, vise à renforcer la compétitivité de la recherche et de l’industrie en Occitanie, Nouvelle Aquitaine et Provence-Alpes-Côte d’Azur dans les secteurs de l’aéronautique, du spatial, et des systèmes embarqués.

Financé à 50% par le secteur public et à 50% par le secteur privé, il réunit les grands industriels de la région des secteurs concernés, les établissements publics et leurs laboratoires pour travailler dans trois domaines technologiques stratégiques : matériaux multifonctionnels haute performance, aéronef plus électrique, systèmes embarqués.

Dans le cadre de son développement, l’IRT recherche un (e) Ingénieur de recherche « vérification et évaluation d’architectures concurrentes » (F/H)

Mission :

Le projet CAPHCA (Critical Applications on Predictable High-Performance Computing Architectures) réalisé à l’IRT Saint Exupéry, a pour objectif la définition et la mise en œuvre d’un processus et de la chaîne d’outils associée permettant l’exploitation sûre d’architectures matérielles multi-cœurs / coprocesseurs modernes, tout en préservant un haut niveau de performances.

Ce projet regroupe plusieurs industriels des domaines de l’avionique et de l’automobile, des fournisseurs de technologies de simulation de plateformes matérielles, et des laboratoires dans les domaines des méthodes formelles, des langages et de l’analyse des systèmes temps-réels.

D’une durée de 3 ans, ce projet s’achèvera en avril 2020. Le contrat porte sur une durée de 18 mois.

Dans ce cadre, le titulaire du poste aura pour mission de définir et de mettre en œuvre les moyens méthodologiques et techniques permettant :

  • de prévenir et/ou détecter les erreurs liées au parallélisme et à la concurrence,
  • d’estimer la performance des différentes solutions architecturales afin de contribuer à guider le processus de conception vers la solution optimale.

Le domaine d’application est celui des applications critiques automobiles et avioniques déployées sur des plateformes d’exécution multi-cœurs récentes (PowerPC, ARM, AURIX,…).

Ces travaux seront guidés par les cas d’étude développés dans le cadre du projet (applications représentatives du domaine de l’avionique et de l’automobile). La démarche sera appliquée, validée et évaluée sur un sous-ensemble de ces cas d’étude.

Les solutions se reposeront sur l’exploitation des modèles de conception logiciels et/ou matériels et sur la mise en œuvre de moyens de vérification formelle (chaîne CADP développée à l’INRIA Grenoble (http://cadp.inria.fr/).

Deux activités sont planifiées ; elles seront réalisées dans l’ordre suivant :

Activité 1 : Vérification d’applications OpenMP

Cette activité a pour objectif de proposer un processus outillé permettant de détecter certaines classes d’erreurs affectant les applications parallèles décrites suivant le standard OpenMP.

On considérera les méthodes d’analyses statiques appliquées aux modèles de conception ou au code et les méthodes basées sur l’analyse des traces d’exécution.

Les activités seront les suivantes :

  • Expression formelle des propriétés de correction liées au parallélisme et à la concurrence (par ex. les « courses critiques » pouvant apparaître dans les applications OpenMP).
  • Etat de l’art des méthodes de détection des erreurs liées au parallélisme et à la concurrence pour les applications OpenMP.
  • Spécification, conception et mise en œuvre d’une approche de vérification des applications OpenMP sur la base des outils de vérification du projet (chaîne CADP).

A noter que ces travaux tireront profit d’autres activités du projet portant sur l’analyse des modèles OpenMP.

Activité 2 : Estimation de performance

Cette activité a pour objectif d’exploiter à des fins d’évaluation de performance certaines des notations, outils, voire modèles formels utilisés initialement à des fins de vérification (notamment dans la première phase des travaux).

On s’intéressera tout d’abord à des modèles déterministes (par ex. pour rechercher la séquence d’interactions conduisant au pire temps d’exécution, pire charge de bus, etc.) puis à des modèles probabilistes et stochastiques. On exploitera les résultats existants exploitant les formalismes LNT et IMC (Interactive Markov Chain), ainsi que des modèles plus classiques tels que les DTMC (Discrete-Time Markov Chains) étendues avec des données.

On exploitera l’ensemble des sources d’information disponibles, telle que les mesures obtenues sur simulateur ou sur cible. On cherchera à intégrer cette démarche de modélisation et d’évaluation à un processus d’exploration et d’optimisation architecturale.

Le travail sera réalisé à l’IRT Saint Exupéry situé à Toulouse. Il sera co-encadré par l’équipe-projet CONVECS de l’INRIA (M. Radu Mateescu). L‘INRIA apportera son support et son expertise scientifique et technique sur les méthodes et outils formels utilisés dans le cadre de ces activités.

En sus de ces travaux spécifiques, le titulaire du poste contribuera à la réalisation des objectifs communs de l’équipe :

  • Rédaction des livrables du projet
  • Publication et / ou présentations dans les conférences du domaine
  • Partage de la connaissance

Profil :

Titulaire d’un doctorat sur l’un des sujets couverts par l’activité (développement parallèle avec OpenMP, vérification formelle par model-checking, modélisation de performance, architectures concurrentes, etc.)

Compétences et connaissances requises:

  • Développement parallèle (notamment : OpenMP)
  • Idéalement : Modélisation formelle pour la vérification : expression de propriétés, description du comportement, etc.
  • Expérience pratique des savoirs théoriques mentionnés ci-dessus

Aptitudes requises:

  • Curiosité, autonomie, capacité de communication (y compris écrite).
  • Intérêt pour la mise en œuvre concrète des technologies (développement logiciel, notamment)

Si cette offre vous intéresse, merci d’adresser votre dossier de candidature (LM+CV) à recrutement@irt-saintexupery.com sous la référence : 18PD-SE-CAPH-01

To apply for this job email your details to recrutement@irt-saintexupery.com

Apply using webmail: Gmail / AOL / Yahoo / Outlook