A Visual Editor for B-Animations
Author
Abstract
The communication between a developer and a domain expert is a very important part in the process of specifying a formal model. 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. However, it is not always easy to discuss a formal model, because understanding formal models written in a specification language like B requires mathematical knowledge a domain expert might not have. A big step forward to facilitate the communication between a developer and a domain expert is already done with the so called animation tools. An animation tool allows to check the presence of desired functionality and to inspect the behaviour of a specification, by "clicking through" the states of the specification. But these tools may still be too difficult for domain experts, because they need also a certain level of knowledge about the mathematical notation to understand the meaning of a specific state. To avoid this communication problem, it is often useful to create domain specific visualizations based on such animations. But creating the code that defines the mapping between a state and its graphical representation is often error prone and a relatively cumbersome task. In this work we introduce the B-Motion 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. The B-Motion Studio frees the user from writing cumbersome code and allows to create the visualization on the "look and feel" principle. Therefore, we developed an easy to use graphical interface. The B-Motion Studio is based on ProB and the Rigorous Open Development Environment for Complex Systems (RODIN). ProB is a toolset combining animation and model checking for B specifications. The B-Motion Studio is able to query the states of this animation and to visualise them. RODIN is an Eclipse-based IDE for Event-B, an evolution of B to specify reactive systems. In this work we support creating visualization for Event-B specifications. However, we made the B-Motion Studio open for other formal languages. For the graphical representation of the states, we use the StandardWidget Toolkit (SWT), which is a powerful graphical widget toolkit for use with the Java platform. Therefore, SWT provides a rich set of widgets like buttons, labels, container.