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

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 83 000 collaborateurs pour un chiffre d'affaires de 19,0 milliards d'euros en 2022, 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 R&D qui préservent les priorités environnementales de sa feuille de route d'innovation technologique.



Safran est dans le top 30 des meilleurs employeurs mondiaux 2022 selon le magazine Forbes.



Safran Electronics & Defense est une société de 10 000 salariés fondée sur la maîtrise de technologies clé au service de la souveraineté. Conjuguant intelligences humaine et artificielle, elle développe des produits et services permettant d'observer, de décider et de guider pour les marchés de l'aéronautique, de la défense et de l'espace. La société met également son expertise électronique au service des autres sociétés de Safran.

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