Skills

Rust GitHub

Job Specifications

Objectif : Développer un workbook à destination des étudiants découvrant la méthode B et l’Atelier B.

Contexte :

L’Atelier B (https://www.atelierb.eu/) est un environnement de développement de logiciel prouvé mathématiquement avec la méthode B. Il est notamment utilisé pour les applications sécuritaires embarquées pour environ un tiers des métros automatiques radiocontrôlés de par le monde. Il connaît un succès non démenti auprès des universités et des écoles d’ingénieur, avec plus de 4500 téléchargements par semestre d’enseignement. Nous avons initié depuis quelques mois une refonte de la documentation destinée aux utilisateurs.

Nous souhaiterions en particulier publier un workbook à destination des étudiants leur permettant de mettre en œuvre l’Atelier B et la méthode B au travers d’exemples complets, de taille raisonnable et de complexité croissante.

Ces exemples couvrent l’analyse de la spécification, la modélisation formelle, la preuve mathématique automatique et interactive, la génération de code, ainsi que l’animation de modèles formels.

Nous disposons de multiples ressources existantes, souvent parcellaires, qu’il faudrait compiler, compléter et documenter, avant que de les intégrer au Worbook. Des exemples complémentaires pourront être extraits d’articles scientifiques et de sites web.

Le workbook est un travail de longue haleine et le stage devra mettre en place les éléments techniques et rédactionnels à suivre pour les prochaines itérations / compléments.

Le stagiaire sera intégré à l’équipe Formation B et en contact avec l’équipe de développement de l’Atelier B.

La langue de rédaction (documentation, modèles) sera l’Anglais.

L’environnement technique est :

B pour la modélisation,
Le langage de preuve (script, règles mathématiques) du prouveur interactif de l’Atelier B,
C pour la génération de code, Rust en option,
Markdown pour le document
Github pour la persistance des données (documentation, archives de projets B, code généré)

Profil recherché
Le stagiaire sera intégré à l’équipe Formation B et en contact avec l’équipe de développement de l’Atelier B.

La langue de rédaction (documentation, modèles) sera l’Anglais.

L’environnement technique est :

B pour la modélisation,
Le langage de preuve (script, règles mathématiques) du prouveur interactif de l’Atelier B,
C pour la génération de code, Rust en option,
Markdown pour le document
Github pour la persistance des données (documentation, archives de projets B, code généré)

Localisation : Aix-en-Provence, Lyon, Paris ou Strasbourg

Durée : 6 mois

Niveau : Bac +5

About the Company

CLEARSY specializes in designing safety critical systems. From design to commissioning, we develop SIL1 to SIL4 certified systems. Our expertise includes data validation, system verification and safety demonstration. Also we promote the formal B method that has the potential to disrupt safety critical system development. CLEARSY proposes solutions to increase passenger flow and safety of the busiest commuter lines, improve train operation safety, reduce costs incurred by safety system development and verify safety critical... Know more