Table of Content
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.
- 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
Bookmarks: save one or several states and recenter the animation on these states at
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.