Brama Presentation, a graphic tool of modelling applied to the B formal method

What is Brama ?

Brama is a tool used to animate B models on the Rodin platform. Brama’s objective is two-fold :

To allow the formal model’s designer to ensure that his model is executed in accordance with the system it is supposed to represent.
To provide this model with a graphic representation and animate this representation in accordance with the state of the formal model. The graphic representation must be in Flash format and requires the use of a separate tool for its elaboration (Flash MX, for example).