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:

• Train Demonstration
• Terminus Demonstration
• DOF1 Demonstration
• Island Demonstration
• Press Demonstration

 

The Tool

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.