Avertissement Ce site n'est pas recommandé pour les navigateurs Internet Explorer. Veuillez utiliser un autre navigateur Web pour profiter d'une meilleure expérience.

Stage - Ingénieur-e logiciel - Spécification et vérification formelles d'algorithmes en TLA+ F/H

Publié
Société : Safran Electronics & Defense Domaine d'activité : Logiciel Emplacement : Massy , Ile de France , France Type de contrat : Stage Durée du contrat : Temps complet Diplôme requis : BAC+5 Expérience requise : Jeune diplômé-e/Première expérience Statut professionnel : Ingénieur & Cadre Langue(s) parlée(s) : Anglais Intermédiaire Fourchette de rémunération : Stage rémunéré
Publié

Parlons de votre future 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é.

Et en complément ?

Asterios Technologies est un fournisseur de solutions logicielles complètes pour le développement de systèmes temps-réel critiques complexes, qui développe et commercialise une solution innovante, à la pointe de la technologie, offrant :
- Des méthodes et outils de conception pour la mise au point des applications temps-réel critiques à forte contrainte de sûreté de fonctionnement ;
- Une plateforme d'exécution temps-réel incluant un micro-noyau sur cible matérielle multi-cœurs.

Basée à Massy (91), Asterios Technologies est présent principalement dans les secteurs de l'aérospatial, la défense, et l'automobile ; et cherche également à s'étendre dans les secteurs ferroviaire, nucléaire et médical.

Créée en 2011, et filiale à 100% de Safran Electronics & Defense depuis juin 2023, Asterios Technologies est une entreprise à taille humaine, évoluant dans un environnement de type start-up avec une agilité qui lui est propre, tout en bénéficiant du rayonnement de Safran.

Dans ce contexte, Asterios Technologies offre la possibilité de s'épanouir au sein d'une équipe R&D autonome et créative, où les méthodes de travail y sont basées sur la collaboration inter-équipes, et où l'ambiance de travail y est dynamique et sympathique. Asterios Technologies offre également des perspectives d'évolutions professionnelles.

Parlons de vous

En fin de cursus Bac+5, spécialisé-e en informatique ou équivalent, vous souhaitez réaliser votre stage de fin d'études dans le développement des logiciels embarqués bas niveau (langages C/assembleur, OS/Drivers, Temps-réel).

Compétences demandées :
• Curiosité pour les méthodes formelles et leur application industrielle,
• Sens de la communication,
• Rigueur,
• Travail d'équipe.

Quelques précisions

La compréhension de l'anglais technique est requise pour ce stage.

Localisez votre futur site

16 avenue Carnot 91300

Massy

Ile de France France

Copier l’adresse
83 000
collaborateurs dans le monde
27
pays dans lesquels Safran est présent
35
familles de métiers