MODERNISATION DU GENERATEUR D’OBLIGATIONS DE PREUVE DE L’ATELIER B
Modernisation du générateur d’obligation de preuve d’Atelier B
Objectif : Moderniser et simplifier le code source du générateur d’obligations de preuve de telle sorte à minimiser ses dépendances externes tout en tirant partie des évolutions récentes du langage C++.
Contexte :
La méthode B est utilisée pour développer formellement des composants logiciels et des modèles de systèmes critiques (B événementiel). Atelier B est un environnement de développement intégré (IDE) pour la méthode B et le B événementiel qui est maintenu et développé par CLEARSY. Atelier B dispose d’un générateur d’obligations de preuve développé en C++ et repose également sur la technologie XSLT et des composants tiers qui ne sont plus supportés.
Le stage est structuré comme suit
- Auto-formation B et Atelier B.
- Prise en main du code source du générateur d’obligations de preuve et de ses dépendances (BAST https://github.com/CLEARSY/BAST, PMMLIB).
- Mise en place du banc de test qui servira à garantir la compatiblité et l’absence de régressions.
- Migration de la phase de génération des obligations de preuve actuellement définie en XSLT vers une implémentation en C++.
- Migration des interactions avec les formats XML vers la bibliothèque TinyXML2.
Contraintes technologiques:
- Le code existant est en large partie développé en C++. Le stagiaire devra savoir naviguer confortablement dans le code existant.
- La documentation devra être rédigée en anglais.
- La gestion de la compilation et des tests sera réalisé en utilisant les outils cmake et ctest (https://cmake.org/).
- Le code sera hébergé sur le serveur gitlab de CLEARSY : le stagiaire doit avoir une bonne maîtrise des commandes git, et devra être capable de reconfigurer la procédure d’intégration continue le cas échéant.
Compétences recherchées :
- Solides connaissances de C++.
- Familiarité avec les technologies XML et XSLT.
- Exposition antérieure à la logique formelle ou aux méthodes formelles.
Localisation : Aix-Lyon
Durée : 6 mois
Niveau : Bac +5
Pour postuler merci d’envoyer un Cv et une Lettre de motivation à l’adresse :