Thèse cifre - compilation prouvée de code avionique parallèle temp-réel critique

Job Description:

Une offre de thèse – CIFRE (PhD) – est proposée au sein d’Airbus Commercial Aircraft pour rejoindre notre département « Logiciels Avioniques », basé à Toulouse, France.

Ce département est un fournisseur interne de logiciels intégrés au sein d'équipements. Les ingénieurs de ce département sont responsables de la conception, du développement, et de la vérification de produits logiciels embarqués critiques (par exemple, les commandes de vol, l'alerte de vol, la communication, l'équipement de maintenance) pour tous les avions Airbus. Ce département est également une chambre de référence en matière de logiciels grâce à des équipes accomplies et expérimentées.

Dans le cadre des activités de recherche menées par le département, vous participerez à la définition de méthodologies et d'outils de vérification de logiciels avioniques.

Votre environnement de travail :

Capitale mondiale de l'aéronautique et capitale européenne de la recherche dans le spatial, Toulouse est une ville dynamique du sud-ouest de la France desservie par un aéroport international. Idéalement située entre la mer Méditerranée et l'océan Atlantique et à proximité des Pyrénées, elle offre de nombreuses possibilités d'activités de plein air !

Parce que nous prenons soin de vous :

* Avantages financiers: Salaire attractif, accords d’intéressement et de participation, plan d'épargne salariale abondé par Airbus, plan d’actionnariat salarié sur la base du volontariat, avec attribution d'actions gratuites en fonction du nombre d’actions souscrites.

* Équilibre vie privée / professionnelle: Des jours de congés supplémentaires pour occasions spéciales et des options de transfert de congés, un comité d'entreprise proposant de nombreuses activités socio-culturelles et sportives et d’autres services.

* Bien-être / santé: couverture complémentaire des frais de santé et de prévoyance (incapacité, invalidité, décès). Selon le site : centre de services de santé, services de conciergerie, salle de sport, application de covoiturage.

* Développement individuel: des opportunités d’évolution et des possibilités de formations nombreuses (catalogue de plus de 10.000 e-formations disponibles en libre accès pour développer votre employabilité, certifications, programmes de développement accéléré, parcours expert, mobilité nationale et internationale).

Chez Airbus, nous vous aidons à travailler, à vous connecter et à collaborer plus facilement et de manière plus flexible. Partout où cela est possible, nous favorisons la flexibilité dans nos modes de travail afin de stimuler l'esprit d'innovation.

Motivation et Objectif de la Thèse :

Dans le contexte de la spécification en Lustre de logiciels synchrones et, plus particulièrement, de l’approche « All-In-Lustre », l'objectif de la thèse est d’assurer que le code d’implantation C multithread produit à partir d'une spécification All-In-Lustre et exécuté sur cible multi-cœurs SMP à cohérence de caches (e.g. ARM, Power, x86), est fonctionnellement correct par rapport à la spécification fonctionnelle Lustre.

Parmi les paradigmes de programmation pour systèmes multi-cœurs, les threads offrent la meilleure portabilité et le contrôle le plus fin sur l’allocation des ressources, permettant ainsi de tirer la meilleure performance garantie du matériel contraint en ressources utilisé dans les applications embarquées. Ils sont le seul modèle de concurrence intégré au langage C, à partir de la version C11 du standard. C11 est ainsi devenu le cadre standard pour la définition de la sémantique du parallélisme bas-niveau en mémoire partagée, et ensuite pour les travaux de preuve formelle à ce niveau. Malheureusement, les threads sont un modèle de calcul non-déterministe et non-compositionnel, rendant difficiles la programmation et l’analyse formelle. Cela explique pourquoi les logiciels multi-threads restent bogués même dans le cadre de systèmes critiques. Par comparaison, les applications de contrôle embarqué (ainsi que d’autres types d’applications spécialisées comme celle du Machine Learning ou du traitement de signal) ont de bonnes propriétés de monotonie, de déterminisme et d’observabilité. Cela permet l’utilisation de mécanismes de synchronisation plus bas-niveau, bien plus efficaces, et permettant l’utilisation d’une synchronisation à grain fin. Cela permet d'avoir pour objectif la correction globale du processus de compilation. C’est sur cette classe d’applications multi-cœurs monotones et déterministes que la thèse se focalisera, car elle inclut le code d’implantation attendu pour les applications de contrôle embarqué « All-In-Lustre » d’Airbus.

Le premier objectif de la thèse est de formellement définir cette classe de programmes.

Le deuxième objectif est d’ensuite développer une théorie et une pratique de la programmation bas-niveau d’applications multi-cœurs hautes-performances déterministes. Devront ensuite être formellement définies les primitives de synchronisation, les patrons de conception, la sémantique formelle et les outils de parallélisation formellement prouvés, allant jusqu’à la construction d’une chaîne de compilation prouvée de Lustre vers C multi-thread.


Vos Défis – Responsabilités Clés :

* Collecter et analyser des données relatives à l'état de l’art, aux exigences industrielles, aux classes de programmes C multi-cœurs déterministes servant de cible pour la traduction d’applications Lustre (et justification des choix par rapport aux besoins Airbus).

* Sur la base des données collectées et analysées, choisir les techniques d’implantation, notamment entre une approche par validation de traduction vs. une approche par preuve de compilateur.

* Étendre les applications du cadre théorique de la Logique de séparation concurrente (et de l'atelier associé Iris) pour (1) couvrir les nouvelles constructions de synchronisations bas-niveau très efficaces à base d’horloges logiques utilisées dans la génération de code de Lopht et (2) permettre la preuve de correction d’un processus de compilation. Mécanisation de la sémantique de la classe de programmes multi-cœurs visés.

* Compléter la chaîne de traduction prouvée existante de Lustre vers C multi-thread. Cela implique la création du nouvel outil permettant de valider la correction de la parallélisation de code C, ainsi que la modification de Lopht pour lui permettre de piloter l’outil de validation.

* Procéder à Intégration logicielle et à évaluation de la nouvelle chaîne de traduction sur une application représentative Airbus.

Votre Boarding Pass – Compétences et Profil Recherchés :

Formation :
Diplôme d'ingénieur en informatique. Une expérience en recherche académique et des publications scientifiques constituent un atout important.

Expertise Technique :

* Expérience de développement logiciel

* Bonne compréhension de l’architecture matérielle multi-coeurs et des hiérarchies mémoire (RAM/ROM/Cache), notamment par l'abstraction qui en est faite par les ISA type ARM, x86, POWER et par le modèle mémoire du langage C11

* Maîtrise du langage C et de la programmation multi-coeurs

* Connaissance de Rocq (anciennement Coq) et du framework Iris, notamment en ce qui concerne la prise en compte du modèle mémoire faible de C11

Connaissances Métier :

* Familiarité avec les approches formelles de développement pour logiciels critiques

Compétences Linguistiques :

* Maîtrise de l’anglais (niveau autonome ou avancé)

Compétences Relationnelles et Collaboration :

* Capacité à communiquer efficacement avec des parties prenantes variées et à aligner les objectifs de recherche avec la vision stratégique d’Airbus

* Fortes compétences en travail en réseau et en collaboration pour favoriser les synergies interfonctionnelles et inter-divisionnelles

Cet emploi exige une connaissance des risques de conformité potentiels et un engagement à agir avec intégrité, comme base de la réussite, de la réputation et de la croissance durable de la société.

This job requires an awareness of any potential compliance risks and a commitment to act with integrity, as the foundation for the Company’s success, reputation and sustainable growth.

Company:

Airbus Operations SAS

Employment Type:

PHD, Research

-------

Experience Level:

Student

Job Family:

Software Engineering