Brama is a tool for animating event-B models. Animation is twofold:

  • verification of the system behaviour
  • animated graphical representation of the modelled system

It has been initially developed for the Rodin platform and extensively used for demonstration purpose. Some nice demonstrations are available:


The Tool

predicateb++Brama is being ported to C++/Qt in order to be integrated to Atelier B 4.1, together with PredicateB++ B predicate evaluator that has been extensively tested through a number of railways data validation projects.