Formal B Model Graphic Animation Tool
Reasons: need to validate the models, need to “present” the models
Our broad experience in using formal tools in industrial settings has led us to formulate a new approach to present models to our clients. The Brama tool supports this approach.
The B Method is extensively used in industrial settings to create proven security software in the context of certification at a SIL4 level pursuant to the EN 61508 standard. It has been used for a few years now to model systems. This new practice has revealed a deficiency. Indeed, when you establish specifications for a system, you must:
- Know what you want
- Ensure that what you want is feasible.
The modeling and proof processes lead to the discovery of specification issues. This is the very advantage of modeling. The B Method has the advantage of being mathematically based, which allows for an unequaled precision in the writing of specifications. However, we have observed that, when faced with a model, our clients and, in general, those who did not write the model, have difficulty in understanding it and in confirming that the model truly represents the system. The completeness and quality of the model may therefore be an issue.
The Brama model animation tool provides a response to this situation, as it may be used by the modeler as he or she progresses in the modeling process. The animation functions allow for the “implementation” of the various events, guards and properties of the model – the modeler may therefore “test” the model.
Graphic Visualization of the System
The approach consists in providing the model author with tools that:
- Represent via graphic drawings and animations the system and its various states
- “Link” these drawings and animations to the various events and B variables of the B models
- Represent with buttons the various interactions between the items that are external to the system and refresh the system’s graphic representation according to these interactions.
The model is not shown to the client as such; it is the graphic representation of the system that is presented, which is effected on the base of the B model itself.
More Details on the Brama Tool
The modeler creates B models with Atelier B, B4free, CompoSys or the Rodin platform, then uses the Brama animation tool to exploit these models. Brama was designed to communicate with Flash tools that are configured with a communication extension delivered with Brama. The modeler’s task consists in representing the system with the Flash tools and in configuring the script that will allow for a dialogue with the Brama animation engine. When the user is satisfied, Brama will allow the user to export the animation realized in the form of files which, once burned on a CD, will allow for the graphic animation to start without prior installation and on any PC with Windows or Linux.
Brama is presented as a suite of Eclipse plugins and a Flash extension that can be used with Windows and Linux. Brama includes the following main modules: B2Rodin: an animation engine (predicate solver), visualization tools for events and B variables, a management module for the automatic linking of events, a management module for variables, predicates and observed expressions and a module to communicate with Flash.
Examples and Feedback
The first examples were developed on the basis of experimental models: mechanical press, island/mainland road traffic, lock, switching and the Ariane nozzle control system.
Our work on these examples allowed for the failures present in the analyzed models to be demonstrated, which confirmed the benefit of visualizing the system to better ensure the accuracy of the model.
The graphic representation task is not enormous: approximately one week to perfect the animation of a model created in two months. The largest model represents 450 events and 17 refinement levels.
Brama tools may be used on a Rodin Open Source modeling platform. A converter transforms the exiting B models into this platform’s format.
For the time being, the Brama tool is most often used to create graphic animations for existing models.
Examples of animations will be presented on this site in the near future.
The tool was presented at Clearsy’s stand on the occasion of this conference.