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.