meeduse
commented
5 years ago Thank you for this evaluation. I agree with you, it is not easy to understand a formal specification, since it requires a training in mathematical notions. This is the major drawback of formal methods. In the case of the B method, the required notions are at least: first order predicate logic, set theory and the substitution theory. The use of Meeduse makes sense in a collaboration between MDE and FM experts. 1) MDE allows to circumvent the poor readability of the formal notations. For example, the truth table and the BDD designed in Sirius are useful to debug the formal specifications, because the end-user can play with the specification and shows its execution step-by-step. 2) FM allows to circumvent the lack of automated reasoning tools of MDE. This is the contribution of Meeduse that we are trying to present for TTC'19.
The MDE expert provides the modeling artifacts, and the FM expert provides the formal specifications, and Meeduse puts all these together. In section 3.6 and also in the conclusion, this idea is discussed.
One interesting research direction is to translate B operations into ATL (or other meta-languages) or vice-versa. I think that ATL is a good candidate because of its abstraction capabilities, in comparison with other tools submitted to TTC'19 and which implemented the transformation in a low level programming language (like Java).
A. Idani
The aim of the Meeduse solution is very clear: to gain proven verification for the models and model transformation rule executions using the formal B method. For a range of applications, I can imagine that this indeed is a significant benefit that Meeduse can bring over other model transformation languages and even more over model transformations written in general-purpose languages.
The paper is well written, easy to read and explains what kind of support one can expect when trying to formalize the model transformation using the B method and Meeduse.
However, not having a strong background in formal methods, I find the specification of the model transformation rules in B very hard to understand. The paper argues that QVT-R is not much better but I think that this is also not the best example to learn from. I acknowledge that Meeduse was not originally intended for model transformation, but there is certainly room for improvements. What about transforming e.g. ATL into such a B specification?