Vous allez être redirigé(e) vers Aerocontact

Recherchez parmi les 236 offres de stage ingénieur aéronautique

STAGE - INGÉNIEUR-E LOGICIEL - SPÉCIFICATION ET VÉRIFICATION FORMELLES D'ALGORITHMES EN TLA+ F/H

Offre de stage publiée il y a 30 jours
  • Entreprise SAFRAN ELECTRONICS & DEFENSE
  • Localisation Massy, Ile-de-France, France
  • Fonction STAGE - INGÉNIEUR-E LOGICIEL - SPÉCIFICATION ET VÉRIFICATION FORMELLES D'ALGORITHMES EN TLA+
  • Type de contrat Stage
  • Date de publication 26-05-2024

Description du poste


Safran est un groupe international de haute technologie opérant dans les domaines de l'aéronautique (propulsion, équipements et intérieurs), de l'espace et de la défense. Sa mission : contribuer durablement à un monde plus sûr, où le transport aérien devient toujours plus respectueux de l'environnement, plus confortable et plus accessible. Implanté sur tous les continents, le Groupe emploie 92 000 collaborateurs pour un chiffre d'affaires de 23,2 milliards d'euros en 2023, et occupe, seul ou en partenariat, des positions de premier plan mondial ou européen sur ses marchés. Safran s'engage dans des programmes de recherche et développement qui préservent les priorités environnementales de sa feuille de route d'innovation technologique.

Safran est la 1ère entreprise du secteur aéronautique et défense du classement « World's Best Companies 2023 » du magazine TIME.



Safran Electronics & Defense est une entreprise internationale de plus de 12 000 collaboratrices et collaborateurs, qui mobilisent expertises et esprit de corps pour concevoir des solutions de haute technologie dans les domaines de l'aéronautique, de la défense et du spatial. En combinant intelligence humaine et technologique, l'entreprise développe les produits et services pour aider les acteurs civils et militaires à observer, décider et guider sur terre, en mer, dans le ciel et dans l'espace. Et ainsi contribuer à un monde plus sûr.


Descriptif mission

La spécification et la mise au point de systèmes concurrents est un problème réputé particulièrement ardu, et occasionne des bugs « dormants » difficiles à débusquer par des campagnes de test traditionnelles. Le langage de spécification TLA+ propose un formalisme mathématique fondé sur une logique modale, permettant de décrire de façon non ambigüe les évolutions possibles et les propriétés souhaitées d'un système, logiciel ou matériel. Associé à un model checker (TLC), il constitue un outil remarquablement efficace pour la mise au point et le déverminage de systèmes concurrents, avant même le prototypage.

L'objectif de ce stage, après s'être familiarisé avec TLA+ et les outils associés (TLC, PlusCal), sera de modéliser différents algorithmes de synchronisation utilisés pour implémenter le micro-noyau temps-réel d'ASTERIOS, dans le but d'en proposer une vérification formelle : communication inter-processus, synchronisations inter-coeurs, ordonnancement. Selon l'avancement, l'utilisation d'un assistant de preuve (TLAPS) pourra être envisagé pour élaborer des preuves formelles de propriétés de sûreté.

Profil recherché


Safran est un groupe international de haute technologie opérant dans les domaines de l'aéronautique (propulsion, équipements et intérieurs), de l'espace et de la défense. Sa mission : contribuer durablement à un monde plus sûr, où le transport aérien devient toujours plus respectueux de l'environnement, plus confortable et plus accessible. Implanté sur tous les continents, le Groupe emploie 92 000 collaborateurs pour un chiffre d'affaires de 23,2 milliards d'euros en 2023, et occupe, seul ou en partenariat, des positions de premier plan mondial ou européen sur ses marchés. Safran s'engage dans des programmes de recherche et développement qui préservent les priorités environnementales de sa feuille de route d'innovation technologique.

Safran est la 1ère entreprise du secteur aéronautique et défense du classement « World's Best Companies 2023 » du magazine TIME.



Safran Electronics & Defense est une entreprise internationale de plus de 12 000 collaboratrices et collaborateurs, qui mobilisent expertises et esprit de corps pour concevoir des solutions de haute technologie dans les domaines de l'aéronautique, de la défense et du spatial. En combinant intelligence humaine et technologique, l'entreprise développe les produits et services pour aider les acteurs civils et militaires à observer, décider et guider sur terre, en mer, dans le ciel et dans l'espace. Et ainsi contribuer à un monde plus sûr.


Descriptif mission

La spécification et la mise au point de systèmes concurrents est un problème réputé particulièrement ardu, et occasionne des bugs « dormants » difficiles à débusquer par des campagnes de test traditionnelles. Le langage de spécification TLA+ propose un formalisme mathématique fondé sur une logique modale, permettant de décrire de façon non ambigüe les évolutions possibles et les propriétés souhaitées d'un système, logiciel ou matériel. Associé à un model checker (TLC), il constitue un outil remarquablement efficace pour la mise au point et le déverminage de systèmes concurrents, avant même le prototypage.

L'objectif de ce stage, après s'être familiarisé avec TLA+ et les outils associés (TLC, PlusCal), sera de modéliser différents algorithmes de synchronisation utilisés pour implémenter le micro-noyau temps-réel d'ASTERIOS, dans le but d'en proposer une vérification formelle : communication inter-processus, synchronisations inter-coeurs, ordonnancement. Selon l'avancement, l'utilisation d'un assistant de preuve (TLAPS) pourra être envisagé pour élaborer des preuves formelles de propriétés de sûreté.

  • Date de début 2024-04-29
  • Durée 6 mois
  • Expérience requise Débutant / Jeune diplomé
  • Salaire nc.
  • Référence 2024137258
  • Secteur d'activité
© ingenieur-aéro est le site d'emploi du Groupe AEROCONTACT dédié aux ingenieurs aéronautique.
Aerocontact est depuis 2003 le leader des sites emploi spécialisés dans le secteur de l'Aéronautique, du Spatial et de la Défense.
Il est également un portail d'actualité couvrant l'intégralité du secteur et en particulier le secteur RH.