GESTION DE LA GENERATION DE CODE DANS ATELIER B
Atelier B est un outil industriel de développement formel basé sur la méthode B. Il permet de spécifier un système, de le raffiner par étapes successives jusqu’à un niveau implémentable, tout en prouvant la cohérence de chaque étape. Il est utilisé dans des domaines où la sûreté est critique, notamment le ferroviaire, le transport urbain automatisé et l’industrie.
La dernière étape de la chaîne est la génération de code : les composants implémentables sont traduits automatiquement en code exécutable (C, Ada, etc.).
Toutefois la notion de composant implémentable dépend directement des capacités du ou des générateurs de code employés dans un projet. Cette notion peut également dépendre de la disponibilité de bibliothèques de logiciel de base pour la plateforme d’exécution cible. Le choix du générateur de code et de la plateforme d’exécution cible impose des contraintes qui définissent ce qu’est un composant implémentable.
Actuellement Atelier B définit de manière rigide la notion de composant implémentable selon des critères syntaxiques et sémantiques indépendamment des outils de génération de code concernés par le projet.
La problématique est donc de rendre la notion de composant implémentable configurable et dépendante du contexte du projet (générateur(s) de code, plateforme d’exécution cible, bibliothèques disponibles) au niveau de chaque projet dans Atelier B.
Objectif du stage :
- Identifier les éléments caractérisant une chaîne complète de génération de code. Décliner ces éléments sur différents projets ayant des générateurs de code différents
- Mettre en place dans Atelier B un mécanisme de configuration de la chaîne de génération de code
- Valider la démarche en déclinant ce mécanisme de configuration sur différents types de projets
Compétences recherchées :
- Bonnes connaissances en génie logiciel et en programmation C et C++, avec des notions de gestion de configuration et d’intégration continue (Git, CI)
- Intérêt pour les méthodes formelles, les langages et les générateurs de code
- Rigueur, autonomie et bonne capacité de rédaction