Présentation de BRama

BRama est un outil qui permet d’animer des modèles B au sein de la plateforme Rodin. L’objectif poursuivi par Brama est double :

  • Permettre à l’auteur du modèle formel de s’assurer que son modèle s’exécute conformément au système qu’il est sensé représenter ;
  • Fournir une représentation graphique à ce modèle et animer cette représentation en fonction de l’état du modèle formel. La représentation graphique doit être au format Flash et nécessite l’utilisation d’un outil tiers pour son élaboration (Flash MX par exemple).

Comment installer Brama ?

Retrouvez notre guide d’installation de Brama.
Retrouvez également toute l’information sur le site dédié à BRama.

Comment utiliser BRama ?

Brama s’utilise de deux manières distinctes :

  • Animation d’un modèle B dans l’environnement Eclipse :
    • Affichage des événements déclenchables,
    • Affichage des variables du modèle et de leur valeur,
    • Déclenchement d’un événement modification de la valeur d’une variable.
  • Animation d’un modèle B par l’intermédiaire d’une animation flash :
    • Association d’animations graphiques flash à un changement d’état ou à u déclenchement d’événement B,
    • Modification de la valeur d’une variable ou déclenchement d’un événement suite à une action de l’utilisateur au niveau de l’animation flash

Animation d’un modèle B dans l’environnement Eclipse

L’animation d’un modèle B nécessite :

  • Un modèle vérifié statiquement (aucun messag d’erreur ne doit apparaître dans la vue “Problems”), composé d’une machine et éventuellement d’un ou plusieurs raffinements.
  • La valuation des constantes déclarées dans les contextes.

La valuation des constantes nécessite donner des valeurs à toutes les constantes, y compris les éléments des ensembles énumérés. Cette valuation peut s’effectuer de deux manières :

    • Par utilisation de B2RODIN, lors de l’importation de modèles B textuels :

Importation modèles B via B2RODIN

    • Par saisie des valeurs des constantes, dans l’éditeur de contexte, au sein de la plateforme Rodin :

Saisie des constantes via RODIN

Animation d’un modèle B par l’intermédiaire d’une animation flash

Une fois que le modèle B est satisfaisant (il est complètement prouvé, son animation a montré que le modèle se comporte comme le système associé), il est temps de construire une représentation graphique de ce système et de l’animer de manière synchronisée avec le modèle B Rodin sous-jacent.

Brama ne construit pas cette animation, c’est au modélisateur de construire sa représentation du modèle, en fonction de ce qu’il veut montrer du modèle. Par contre, Brama fournit les éléments qui vont permettre de connecter votre animation flash et votre modèle B.

Pour plus de détails, se reporter à l’aide en ligne de l’outil.

Historique des Versions de Brama

  • 0.0.16 :
    • Amélioration des messages d’erreur.
    • Support des fonctions. Brama est maintenant capable de rechercher des valeurs pour des fonctions.
    • Modifications du tri des événements et ajout d’un bouton permettant de trier les variables.
    • Meilleur support de MacOS X.
  • 0.0.15 :
    • Correction d’un bug empêchant les schedulers de fonctionner sous MacOS
    • Ajout d’un bouton permettant de trier les variables dans l’animateur.
    • Ajout d’un menu “animer” pour les fichiers *.mch et *.ref. Cette commande convertit le fichier B en fichier rodin, et lance l’animateur sur le fichier converti.
  • 0.0.14 :
    • Amélioration importante des performances