Review of Meeduse

[rene-schoene]

Tool

• Installation procedure very easy to use for an Eclipse solution, and successful for me on Fedora 29
• Usage (starting the actual transformation) requires quite a few steps, which should be one transformation step. I was able to get the first models transformed, but failed on one of the larger ones (process of transformation did not finish within an hour, which was reported 18minutes in the paper)
• No integration in the benchmark structure provided by the case, thus difficult to access metrics like execution time, number of nodes for myself
• The video tutorials were very helpful for executing the first transformation

Paper

Contents

The paper describes Meeduse, which combines formal methods (e.g., verification) and model driven engineering. It is usually used to describe execution semantics of DSLs, so the objective was to map its original intend to this case (model transformation). The objective was not to find most compact BDT, and the update of case description discovered too late, thus was ignored.

Review

In general, the paper was very good to follow and provided a good description of the tool itself, its "normal" application, and its usage within the TTC case.
There are some additional remarks:

• From Figure 1 it is not clear on at first sight, how the B machine is created, since apparently it comprises multiple steps (first creation from meta model, then optional refined, finally injection using model)
• Figure 3: Attribute "done" is required, but later in text described as optional
• For the execution times, hardware specifications and number of iterations are missing. Also redundant information in the result table can be omitted (name can be derived from input and output ports, rows is always equal to "2 to the power of input rows")
• The whole paper was written in a tutorial style, which was perfectly fine for reviewing the tool and get used to the concepts. For the final version of the paper (with a limit of 5 pages), I'd advise to put an emphasis on the actual transformation rules, like shown on p.14. However, those rules are currently not easy to understand as notations like "cellPort ^ -1", the row selection "[{TRUE}]" or the symbol "\rhd" (the triangle pointing right). As the step-by-step tutorial probably is too large, the merged meta models of the actual case could be of interest.
• One point remains unclear to me (at least for the example case with persons): As you specify the transformation rules by hand using proven constructors, there can be errors in this specification. Later you claim, that the output model does not need to be verified. I suppose, correctness w.r.t. to the meta model is verified, e.g., that cardinalities are adhered to, bidirectional associations are handled correctly, etc. However, the semantic correctness is ensured using invariants, to, as you wrote, "have some confidence about its correctness". Maybe you should emphasize these different aspects of correctness, i.e., adherence to the meta model, correct transformation, and the way how they are ensured (by construction, and using invariants).

Questions independent of the case which could be discussed on site

• Concerning performance
  • Is there a possibility to specify the order in which rules are applied? This may speed up execution as there won't be a non-deterministic choice which rule to apply.
  • Why is it necessary to run a verification after each transformation step (stated on p.17)?

Minor remarks

• Figure and Section should be capitalized, can use package cleverref for this
• p2. "Proof of correction" should be "Proof of correctness"?
• p3. "Injector: [...] an translate" → "[..] and translate"

Metrics

1. Does the solution use the provided benchmark structure, i.e., is a batch execution supported?
   → No
2. Can all models be transformed within 10 minues?
   → No (10/2 = 18min as of the paper but not reproducable, 12/2 = 6h 40min as of the paper, 14/4 = GC overhead)
3. What kind of result is produced? BDT, BDD, with fix order
   → BDT (old case) using algorithm of case
4. Is the transformation correct?
   → Yes, and proven (adherence to meta model by design, semantics checked by model checker using invariants)
5. Computed Metrics (like number of decision or assignment nodes)
   → unknown

[meeduse]

First, I would like to thank you for these valuables comments. We give you some answers below, in order to clarify some of your interrogations:

1. Attribute done is optional. The meta-model should be graphically modified. This issue comes mainly from EMF which needs some enhancements. Indeed, even if the attribute is optional, when the user instantiates a class, EMF automatically assigns to it a value. For integer attributes, it puts by default a 0 initial value which is not defined neither in the MOF standard, nor in the UML standard. We claim that our formal modeling of the meta-model is more conformant to the MOF standard, than EMF itself.
2. "As you specify the transformation rules by hand using proven constructors, there can be errors in this specification" : My answer is yes, and that's why we apply proofs all along the transformation process. This is explained in section 3.5 showing how the transformation can proved correct. Since the transformation rules (written as B operations) use proved modeling operations (generated from the meta-model), then it will never produce a model which is structurally incorrect. Hence, it is not necessary to use the EMF validator. Regarding the semantic correctness, it is done by model-checking basing on the transformation properties that we identified (in form of goal, assertions and invariants). They are not formally presented in the document in order to ovoid more complexity. We presented them informally.
3. "Is there a possibility to specify the order in which rules are applied?" Yes, but our objective is not execution, but correctness. From this point of view, if you specify an order you will never cover all the state space and then you may miss several possible output models. In our approach, the model-checker covers all the state space, which means that it gives all possibles solutions, which means also that all possible solutions are checked correct mathematically. If the objective is one deterministic execution, in order to have one solution, then the other tools are more suitable than Meeduse, even if Meeduse allows also to execute the transformation.
4. "Why is it necessary to run a verification after each transformation step (stated on p.17)?" Our objective is to apply M2M transformation for safety critical systems and show how this can be assisted by tools. TT and BDD are used in railway mechanisms, in nuclear reactor controllers, etc. For these kinds of systems all the state space must be safe, because any failure may lead to human loss. You cannot expect any safety from a system with incorrect intermediary states even if the last state is correct. A train can move from one train station to another. Showing the reachability of the last train station is not sufficient. This is exactly what happens when you check only one output BDD from a set of 5 or 6 input TT models. Obviously, the movement of trains is not safe if it violates the intermediary signaling mechanisms and this is exactly the kind of failures that a model-checking technique looks for. Our formal transformation rules, not only maintain a correct input and output models, but also guarantees the safety of all reachable states.
5. "10/2 = 18min as of the paper but not reproducable" : for big examples without unfilled cells, you need to run the model-checker from outside Meeduse (see the third video), with: SET PREF MAX OPERATIONS == 1, which tries only one operation (described in the paper). Also the maximality mechanism developed in the paper must be deactivated (comment lines "∧ maxPort(port, selectedRows)" and "∧ maxPort(portBis, selectedRows)"). We should add a documentation for that in our repository.