Open rene-schoene opened 5 years ago
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. 4) "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.
Tool
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:
Questions independent of the case which could be discussed on site
Minor remarks
cleverref
for thisMetrics