Meeduse: A Tool to Build and Run Proved DSLs

Executable Domain-Specific Languages (DSLs) are a promising paradigm in software systems development because they are aiming at performing early analysis of a system's behavior. They can be simulated and debugged by existing Model-Driven Engineering (MDE) tools leading to a better understanding of the system before its implementation. However, as the quality of the resulting system is closely related to the quality of the DSL, there is a need to ensure the correctness of the DSL and apply execution engines with a high level of trust. To this aim we developed Meeduse, a tool in which the MDE paradigm is mixed with a formal method assisted by automated reasoning tools such as provers and model-checkers. Meeduse assists the formal definition of the DSL static semantics by translating its meta-model into an equivalent formal B specification. The dynamic semantics can be defined using proved B operations that guarantee the correctness of the DSL's behavior with respect to its safety invariant properties. Regarding execution, Meeduse applies the ProB animator in order to animate underlying domain-specific scenarios.