Event B Model Animation Tool Brama

Une annonce de Thierry Lecomte de la société Clearsy
relative à la méthode B. Pour avoir une idée de
ce que l'on peut faire, exécutez les exemples fournis :
Flash animations examples are available at:
http://www.brama.fr/html/animations_en.htm



Dear all,

The Event B Model Animation Tool Brama
(beta 1 version)
 is available for
download at:
http://www.brama.fr/html/telecharger_en.htm.

This tool enables animating event based
B models, within the Rodin platform.
Event B compliant, Atelier B models
can be imported using b2rodin plugin (see
http://www.bmethod.com/html/outils_en.html).

Animation capabilities are twofold:

- Debugging B models: the design
 can verify by experiment that a model
and a system have similar behaviour.
- Connecting B models with flash
 animation: B models are used to trigger
flash animation.

Setup and use Information are available at:
http://www.brama.fr/html/telecharger_en.htm

Flash animations examples are available at:
http://www.brama.fr/html/animations_en.htm

Dedicated tool forum is located at:
 http://http://bmethod.com/forum