GENERATION DE CODE PROUVE EN RUST

Objectif du stage : Développer un traducteur de modèles formels B vers le langage Rust

CLEARSY est une PME Française fondée en 2001 par les ingénieurs auteurs de l’industrialisation de l’outil de modélisation formelle appelé Atelier B, utilisé pour spécifier, concevoir, valider les systèmes et réaliser les logiciels critiques (comme le pilote automatique du métro de la ligne 14 à Paris).
L’activité est majoritairement orientée vers le secteur ferroviaire, énergie (nucléaire) et défense.

Société à taille humaine sur 4 sites en France, en pleine croissance (150 personnes), nous développons et déployons nos systèmes dans le monde entier depuis plus de 10 ans, nous avons notamment pu travailler à Sao Paolo / Stockholm / Caracas / New York / Hiroshima / Honolulu…)

Les équipes CLEARSY interviennent dans toutes les phases d’un projet, de la spécification à la réalisation de systèmes « clé en main » tout en garantissant un respect le plus strict des exigences de sûreté.
Clearsy recherche aujourd’hui des ingénieurs passionnés par le challenge technique et qui ont appris à apprendre pour venir renforcer ces équipes techniques.

Cette citation reflète bien nos valeurs : Steve Jobs – Cela n’a pas de sens d’embaucher des gens intelligents et de leur dire quoi faire ; nous embauchons des gens intelligents pour qu’ils nous disent ce qu’il faut faire

Atelier B est un environnement de développement de logiciel avec la méthode B, une méthode de développement logiciel basée sur les méthodes formelles. Elle repose sur la preuve mathématique qu’une implémentation logicielle correspond à sa spécification, exprimée dans un langage formel. L’implémentation logicielle dans la méthode B est exprimée dans un sous-ensemble du langage B, langage de programmation impératif appelé B0. Des traducteurs vers les langages C et ADA permettent ensuite de générer des implémentations dans ces langages.
Dans le cadre de sa démarche de conception de systèmes sécuritaires, CLEARSY souhaite développer un traducteur de modèles B vers le langage Rust. Ce stage pourra s’appuyer sur des outils internes similaires existants ou donner lieu à un développement original, en fonction de l’aisance et de l’appétence du stagiaire avec les formalismes et technologies utilisés.

Mission :

• Spécifier les schémas de traduction de B0 vers Rust,
• Développer l’outil de traduction de B0 vers Rust,
• Construire et mettre en œuvre le banc de test qui permettra de valider le traducteur, sur des exemples simples et sur des (extraites de) projets industriels,
• Rédaction du manuel utilisateur de l’outil de traduction de B0 vers Rust (langue anglaise).

Compétences recherchées :

• Développement C++
• Git
• Expérience de la programmation Rust (savoir ce qu’est un bon programme)
• Bonnes capacités d’expression écrite et orale
• Rigueur, autonomie, force de propositions
• Connaissance en sémantique des langages de programmation serait un plus

Localisation : Aix en Provence
Durée : 6 mois
Niveau : Bac +5

Pour postuler merci d’envoyer un Cv et une Lettre de motivation à l’adresse stages-ingenieurs@clearsy.com