>

Accueil l L'Outil BramaTélécharger l Démos en ligne l Documentation l LiensContact   


Télécharger Brama

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 message 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 :

  • par saisie des valeurs des constantes, dans l'éditeur de contexte, au sein de la plateforme 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.