[Rodin-b-sharp-user] EMF for Event-B for M2M transformation

[Ulyana T. <uly...@gm...>]

Dear Rodin developers,

Thank you for the nice tool! It is so good to be able to check all my
formal specifications on flight with Rodin.
I have a question concerning generating Event-B models automatically.

We are using Event-B and Rodin tooling to specify semantics (behavior) of a
DSL (domain specific language). The idea is to generate Event-B models from
our DSL models (programs) automatically and then to use Rodin-based
proving, animating and model-checking to verify these DSL models. Our DSL
is implemented using EMF (Eclipse Modeling Framework) and has
an explicit ecore metamodel therefore. So I would like to apply
model-to-model transformation (with QVT or ATL) for the task. For that I
need to be able to instantiate Event-B models in EMF style. I assume that
the project "EMF framework for Event-B" can provide me with this
functionality.

So I installed EMF framework for Event-B, but I can not do anything with it
(I can not even create a model-file from "Example EMF Model Creation
Wizards"). Is there any tutorial on the usage of this plug-in? Or could you
please help me with any other tips concerning model-to-model transformation
targeting Rodin?

Thank you in advance,
Ulyana Tikhonova,
Eindhoven University of Technology.