Overview of Meeduse

Meeduse is a Language-Workbench dedicated to formally instrument Domain-Specific Languages using the B-Method, which allows automated reasoning about the correctness of a DSL. The tool is built on EMF and ProB, an animator and model-checker of the B-Method. Several features are provided, such as verification, animation and debugging.

• Credentials:
• Contributors: Akram Idani, German Vega
• Contact: akram.idani at univ-grenoble-alpes.fr
• Webpage: http://vasco.imag.fr/tools/meeduse/
• Reference papers:
• Akram Idani, Yves Ledru, German Vega. Alliance of Model Driven Engineering with a proof-based Formal Approach. Innovations in Systems and Software Engineering (ISSE), NASA Journal. Springer, December 2020, Volume 16, number 3. https://doi.org/10.1007/s11334-020-00366-3.
• Akram Idani. Meeduse: A Tool to Build and Run Proved DSLs. Integrated Formal Methods (iFM'20). https://doi.org/10.1007/978-3-030-63461-2_19
• Update sites:
• B4MSecure: http://vasco.imag.fr/tools/b4msecure/updates/build
• Meeduse: http://vasco.imag.fr/tools/meeduse/updates/build
• License: Meeduse is distributed under the EPL v1.0 license.

Main features

• Meeduse can be used with EMF-based DSL builders such as Xtext, Sirius and ECore. The following screenshot shows both a textual and a graphical model (Views 1 and 2). The other views are provided by Meeduse for interactive animation, debugging and verification.


• the execution history view (3) allows an omniscient debugging, which is useful to go backward in time and manage the execution traces;
• the execution view (4) provides valued B operations that can be applied to the current model; these operations are computed by ProB;
• the command-line console (5) is for interactive debugging;
• the state view (6) computes the various valuations of the B data structures and informs the user whether the invariant properties are preserved or not.

• Meeduse offers several useful facilities:


• Model-checking: ensured by ProB in order to find invariant violations, look for the reachability of pre-defined goals, find deadlocks, etc.
• Interactive animation: provides a step by step execution of the model.
• Random animation: randomly triggers B operations and provides an automatic execution of the model
• Bookmarks: save one or several states and recenter the animation on these states at any time.
• Trace replay: to replay (backward or foreward) execution traces so that the origin of a defect can be understood.
• Reset: at any time one can reset a model and go back to the original one.
• Console: to evaluate (by hand or on-the-fly) B expressions.

Gallery