Intégration de B4SYN dans l’Atelier B

Le but de ce stage est d’intégrer le générateur de code B4SYN dans l’Atelier B (https://www.atelierb.eu/).
B4SYN est un générateur de code, traduisant un projet Event-B (fichiers bxml) en un modèle VHDL. Il a été co-développé avec STMicroelectronics en 2009 et utilisé avec succès sur un cas d’application grandeur nature (http://goo.gl/n61dS3).

L’intégration doit être :

  • fonctionnelle: il faut coupler le fonctionnement du générateur de code, développé en Prolog, à l’Atelier B.
  • graphique: il faut définir une interface graphique et des modalités d’interaction avec l’utilisateur.

Le stage consiste à:

  • s’assurer que B4SYN puisse être utilisé par l’Atelier B (le générateur de code est écrit en Prolog)
  • développer une IHM qui permette d’utiliser l’outil et d’interagir (transformation terminée, erreurs de traitement, non-conformité avec modèles implémentables supportés)
  • développer une fonction de vérification de conformité du modèle B avec les exigences du générateur de code.
  • sélectionner/produire quelques exemples de modèles Event-B représentatifs
  • tester ces modèles dans la chaine de production de code
  • vérifier que le code produit passe dans une chaîne de traitement VHDL (Modelsim Altera Starter Edition)
  • rapporter les erreurs rencontrées. Celles-ci seront a priori corrigées en dehors du cadre du stage.
  • documenter l’outil : documentation de conception, documentation utilisateur non commerciale (la version commerciale sera réalisée en s’appuyant sur celle-ci).
Location
  • Aix-en-Provence
Duration 4 à 6
Level 5

Postuler à cette offre de stage d'ingénieur

Pour postuler merci d’envoyer
un CV et une lettre de motivation
à l’adresse :

stages-ingenieurs@clearsy.com