Generating Domain-Specific Interactive Validation Documents

In state-of-the-art approaches, requirements are gradually encoded into the model, with each modeling step being verified. Once the modeling and verification process has finished, code generation is usually applied to generate the final product. Finally, the generated code is validated, e.g., by executing tests, or running simulations. At this point, stakeholders and domain experts are actively incorporated into the development process. Especially in industrial applications, validation is as important as verification. Thus, it is important to integrate the stakeholders' and the domain experts' feedback as early as possible. In this work, we propose two approaches to tackle this: (1) a static export of an animation trace into a single HTML file, and (2) a dynamic export of a classical B model to an interactive HTML document, both with a domain-specific visualization. For the second approach, we extend the high-level code generator B2Program by JavaScript, and integrate VisB visualizations. An important aspect here is to ease communication between modelers and domain experts, which is achieved by implementing features to share animated traces, and giving feedback to each other.