From BMotion Studio
BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. BMotion Studio frees the user from writing code and allows to create the visualization on the "look and feel" principle.
BMotion Studio is based on ProB and integrated into the Rigorous Open Development Environment for Complex Systems (RODIN). It supports creating visualizations for Event-B specifications. However, BMotion Studio is open for other formal languages.
Commercial support is provided by the spin-off company Formal Mind.
Formal methods like the B-Method gained a lot of popularity as approach for the specification and design of software that ensures its safety and reliability. Several industrial projects like the Coppilot System that controls the opening and closing of platform screen doors at the paris metro line 13 have been installed successfully. Such industrial applications need also industrial strength tools in order to support the deployment of formal models. One of them is ProB. ProB is an animation tool with the challange to check the presence of desired functionality and to inspect the behavior of a formal model.
Another challenge for successful deployment of formal models is the communication between a developer and a domain expert (or manager). On the one hand it is crucial for the developer to get feedback from the domain expert for further development. On the other hand the domain expert needs to check whether his expectations are met. Furthermore, good communication and presentation of formal models can help to obtain several contracts. An animation tool could perform this task, but may be still too difficult for domain experts, because they also need a certain level of knowledge about the mathematical notation to understand the meaning of a specific state. To avoid this problem, it is useful to create domain specific visualizations.
That's why we introduced BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert.