Présentation de la société : SNCF

Le système de signalisation ferroviaire permet aux trains de circuler en sécurité sur un réseau ferré constitué d'équipements multiples. Il gère les signaux (les feux de signalisation se trouvant le long des voies) et les appareils de voie (les aiguillages) de sorte à n'autoriser le passage des trains que lorsque les conditions de sécurité nécessaires à ce passage sont établies. Autrefois mécaniques, puis électriques (par le biais de relais) , le système de signalisation est maintenant en partie informatisé.

Ce stage s'inscrit dans un projet, en partenariat avec le LaBRI (Laboratoire Bordelais de Recherche en Informatique) .

L'objectif de ce stage est de modéliser un nouveau système de signalisation et d'en vérifier les propriétés : absence de deadlock, absence de livelock et safety. Le modèle devra permettre de réaliser du model-checking ainsi que de la simulation.

Des connaissances dans l'algorithmique distribuée, les bases de données distribuées, technologie innovantes (blockchain…) ainsi que la modélisation des systèmes asynchrone seraient un plus.

Missions

Spécialité : Informatique / Méthodes Formelles

Participer à la conception détaillée du nouveau système de signalisation,

Réaliser un outil d'instanciation des modèles de signalisation

Identifier et formaliser des règles d'instanciation des propriétés à vérifier (absence de deadlock, livelock, …)

Réaliser un outil d'instanciation des propriétés de sécurité,

Cartographier et analyser la base de données de description de l'infrastructure,

Réaliser un outil d'instanciation du nouveau système de signalisation,

Intégrer le modèles et les propriété au sein d'un outil de model-checking.

Profil recherché

Bac+5 Information spécialité Modélisation / Méthodes Formelles

Connaissances spécifiques

Bonne capacité d'abstraction et d'apprentissage,

Bonne expérience de programmation en Java, OCaml ou équivalent,

Intérêt pour les méthodes formelles appliquées à l'ingéniérie.