HOME Update Site PAPERS User's Guide

Job Offer: PhD position [pdf]

FeverTokens, in collaboration with the LIG lab and Télécom SudParis is looking for a PhD candidate for a 36-month contract in the domains of Block-chains, Formal Methods (FM), and Domain-Specific Languages (DSLs).

Contact: akram.idani at univ-grenoble-alpes.fr

Meeduse is a hosted Language-Workbench dedicated to formally instrument Domain-Specific Languages using the B-Method, which allows automated reasoning about their correctness. The tool is built on EMF (the Eclipse Modeling Framework) and ProB (a powerful animator and model-checker of the B-Method), providing features for verification, animation and debugging.

User's Guide
  • Meeduse can be used with EMF-based DSL builders such as Xtext, Sirius and ECore. It provides four main views:

    • Trace view: allows an omniscient debugging, which is useful to go backward in time and manage the execution traces;
    • Execution view: provides valued B operations that can be applied to the current model; these operations are computed by ProB;
    • Command-line console: is for interactive debugging;
    • Sate view: computes the valuations of the B data structures and informs the user whether the invariant properties are preserved or not.
  • 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.