X

Job Offers

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

IRT Saint- Exupéry

Département: Systèmes Embarqués

N+1: Responsable de Pôle

CDD : 18 mois

Lieu : Toulouse

L’Institut de Recherche Technologique Saint-Exupéry (Aéronautique-Espace-Systèmes Embarqués), vise à renforcer la compétitivité de la recherche et de l’industrie en Midi Pyrénées et Aquitaine 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 Ingénieur de recherche «  évaluation et vérification formelle d’architectures concurrentes » (H/F)

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 chaine 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.

Dans ce cadre, l’Ingénieur de Recherche 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).  Les résultats seront évalués sur un sous-ensemble de ces cas d’étude.

Les solutions se reposeront sur l’application de modèles et de moyens de vérification formels issus, si possible, des modèles de conception logiciels et ou matériels (modèles AADL, HOOD, UML, etc.). L’Ingénieur de Recherche contribuera au choix du ou des formalismes de conception afin de faciliter cette transition. Le modèle formel exploitera les langages et outils de la chaîne CADP développée à l’INRIA Grenoble (http://cadp.inria.fr/).

La démarche sera appliquée et validée sur tout ou partie des cas d’étude définis dans le projet.

Les activités de l’Ingénieur de Recherche s’organiseront en deux phases d’une durée approximative de 9 mois chacune.

Phase 1 : Exploitation pour la détection des erreurs de concurrence

Cette phase des travaux a pour objectif de proposer une démarche outillée permettant de détecter certaines classes d’erreurs sur la base du modèle de conception. Deux approches seront étudiées voire combinées : (i) une approche basée sur la définition de patrons d’interaction, la vérification formelle de ces patrons, et leur exploitation pour constituer une application, et (ii) une approche basée sur la vérification directe du modèle architectural de l’application.  Les formalismes architecturaux seront définis au cours du projet. Le choix sera notamment guidé par les capacités de vérification. Le formalisme AADL du SAE est un candidat possible.

Pour les familles d’applications retenues dans le projet, les activités seront les suivantes :

  • Analyse des modèles d’exécution et de communication
  • Contribution à la définition de patrons de conception pour l’expression du parallélisme et de la concurrence. Ces patrons s’appuieront sur les mécanismes proposés par les API de parallélisation standards (MT-API, OpenMP, etc.).
  • Expression formelle des propriétés liées au parallélisme et à la concurrence
  • Modélisation et vérification formelle des patrons de conception
  • Application de ces patrons à un ou plusieurs cas d’utilisation

On s’intéressera aussi à l’usage combiné de cette approche avec d’autres méthodes telle que l’interprétation abstraite, par exemple.

Phase 2 : exploitation des formalismes et outils du model-checking pour l’estimation de performance

Cette phase des travaux 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, l’Ingénieur de Recherche 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é (model-checking, modélisation de performance, architectures concurrentes, etc.)

Compétences et connaissances requises:

  • Modélisation formelle pour la vérification (expression de propriétés, description du comportement).
  • Techniques de vérification par model-checking
  • Modélisation de performance (modélisation probabiliste, stochastique, …)
  • Architectures parallèles concurrente, langages et/ou API de programmation parallèle (OpenMP, MTAPI, etc.)
  • Utilisation d’outils de modélisation et de vérification par model-checking (CADP, Tina, Romeo, Uppaal, etc.)
  • Développement logiciel et expérimentation

Aptitudes requises:

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

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

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

Apply using webmail: Gmail / AOL / Yahoo / Outlook