Our objective is not to search for the most compact BDD, but to show how a formal method assisted by automated reasoning techniques can be applied for the particular eld of model transformation. 2
We advocate for collaborations between the formal methods (FM) community and the model-driven engineering
(MDE) community in order to take bene ts of their complementarities. The Meeduse2 tool favors this
communication since it makes possible the use of MDE and FM tools together in one uni ed framework and supports
a pragmatic approach for mixing model-driven engineering with a proof-based formal approach. In practice,
the tool brings together two technological spaces: EMF for model driven engineering and the B Method [1] for
theorem proving and model-checking. The tool is built on top of three components:
(
As Meeduse was not initially designed to de ne model transformation rules, but to de ne DSL execution semantics, we need to rethink the model transformation problem in terms of operational semantics of an abstract machine. The global strategy consists in reusing the Translator component to help automate the writing of the formal speci cation of the transformation, and apply the Meeduse's Animator synchronization capabilities to produce the resulting EMF output model from a given input model. 3 3.1
The input of Meeduse is the meta-model of a DSL and hence in order to apply the tool for model-to-model transformation, we rst need to merge both input and output meta-models into a single one as presented in Figure 1 where the left hand side presents the TT meta-model and the right hand-side presents the BDD meta-model. We suggest that the execution semantics of the transformation follows a consumption/production technique: instances of output classes are created while consuming instances of input classes. In order to keep track of the modeling elements that have been processed by the transformation, we introduce an abstract metaclass Element which allows to gather modeling elements consumed by the transformation. This class introduces an attribute name to identify processed elements. We also introduce a Boolean attribute selected inside class Cell in order to mark cells being processed by the transformation. Having de ned this merging meta-model, we are ready to start thinking about the formalization of the transformation.
2Meeduse: Modeling E ciently EnD USEr needs. From the merging meta-model, Meeduse automatically generates B speci cations that gathers modeling operations as well as structural invariants. This technique allows to write later the transformation rules in the B language. The Meeduse rules for translating an Ecore meta-model into a B speci cation can be roughly summarized as following:
Primitive types (e.g. integer, boolean) become B basic types (Z, BOOL,. . . ).
For each meta-class there is a variable in the speci cation (named as the class) representing the set of existing instances (e.g. variable Row represents the set of existing instances of class Row). If a class A is a subclass of a class B then Meeduse generates an inclusion relationship between their corresponding existing instances (A B). For example, we get predicate InputPort Port because class InputPort is a sub-class of class Port. The additional class Element introduced in the merging meta-model is translated into an abstract set that represents all possible instances.
Each attribute leads to the de nition of a variable that is typed as a function from the set of possible instances to the attribute type (e.g. Cell value 2 Cell ! BOOL). The function specializations depend on multiplicities and the optional/mandatory character of the attribute. For example, attribute selected in class Cell is an optional Boolean attribute, and the corresponding variable is a partial function de ned as: Cell selected 2 Cell !7 BOOL.
Associations are represented as functional relations between the sets of possible instances issued from both source and target classes (e.g. tree owner 2 Tree 7 BDD ). Like attributes, the relation depends on the reference cardinalities (and its opposite) like for example, the tree owner variable which is a partial injection specifying the association between classes Tree and BDD with multiplicity 0..1 in its two extremities.
The behavioral part of the generated B machine provides all basic operations for model manipulation: getters, setters, constructors and destructors; for this reason we refer to this machine as the \model construction" machine. Note that this step is similar to what happens in MDE tools that generate code from meta-models. For instance, from a given meta-model, EMF generates Java modeling code (getters, setters, etc), that can be used to program model transformation in Java. In the same way, Meeduse generates a B machine that can in turn be used to specify model transformations in B. The B speci cation generated automatically from the merging meta-model is about 1162 lines of code with 89 basic operations which are proved correct (with respect to the structural invariant) by construction. Proofs were carried out using the theorem prover of AtelierB which generated 260 proof obligations. This means that the use of the modeling operations guarantees the preservation of the structural properties (invariant) of the meta-model and they will never create an invalid instance contrary to a Java-based technique like that of EMF or other tools. 3.3
The model transformation is manually written in a new B machine as a set of B operations that call the modeling operations generated in the previous step. Each transformation rule is de ned as a B operation composed of two parts: the guard and the action. The guard gives the conditions under which the rule can be triggered, and the action speci es a sequence of calls to modeling operations. Since the individual model construction operations (constructors, setters, . . . ) were proved correct, the result of executing a sequence of operations in the action part of a rule will obviously preserve the model structural properties. The B speci cation of the transformation gathers three main B operations (see Appendix for details):
TruthTable2BDD: this rule creates a BDD from a truth table under the condition that the BDD was not previously created. It also creates the BDD input and output ports, and then adds all generated ports to the BDD. It sequentially calls modeling operations BDD NEW, BddInput NEW, BddOutput NEW and BDD Addports which were generated from the meta-model.
SelectPort: this rule selects an input port satisfying a maximality condition that depends on the current state of the transformation and then decides whether it creates a new tree or reuses a tree already created. When it creates a tree it calls the modeling operation Subtree NEW. For the rst tree it only calls Tree SetOwnerBDD which marks this rst tree as a root tree. These are the rst actions that the operation makes. The next actions non-deterministically select cells of value zero or one which leads to two possible instances of operation SelectPort that can be applied to the same selected port.
Transform: this operation can be triggered only when there is no more than one selected row, and allows to consume the row together with its cells. It has two deterministic behaviours: creates an assignment for output cells if there exists an output cell not yet consumed, or creates a leaf if all output cells are consumed.
In order to verify the correctness of our rules we introduce invariants that de ne the transformation properties and we apply a model-checking proof in order to check for the existence of a sequence leading to violations. Since we deal with a bounded state-space, this proof is su cient as far as the state-space is entirely covered. The ProB model-checker computes exhaustively all the execution possibilities and checks the reachability of unwanted states using the following goals:
For every output cell of a consumed row, one assignment is created with the same value.
Values of trees in a computed BDD path are equivalent to the selected cells values in the consumed row.
Our exhaustive model-checking validation technique was done on input models of reasonable sizes: until 5 input ports, 2 output ports, and 32 rows. We believe that the model-checking proofs done given these models are su cient to have con dence about our rules because most of the provided models are generated by a combinatorial technique. We think that since the proof succeeded for a restricted number of port combinations, then it can be generalized for bigger combinations. Not only the algorithm applies redundantly the same principles to the consumed rows but also the properties of these rows (by means of cell values and connexion with ports) are similar and they don't change during the transformation.
Further study may be required in order to show the existence of a least xed point, from which one can generalize the proof and stop building input models for the exhaustive model-checking. For bigger examples we simply apply Meeduse as a runner of the transformation in order to get the output BDD. For these examples we set property SET PREF MAX OPERATIONS to one, which forces ProB to compute only one instance of each operation which is immediately animated by Meeduse in the automatic execution mode. Finally, we note that all our output models successfully passed the validator provided by the TTC'2019 organizers which was somehow expected since we checked the B speci cations using automated reasoning tools. Meeduse was also helpful for debugging the formal speci cations thanks to the visualization designed in Sirius. 4
Proofs are mainly for veri cation purposes (i.e., \is the transformation correct?"). However, we need to validate the rules in order to be sure that they produce the results expected by a domain expert (i.e., \is this the right transformation?"). For this purpose, Meeduse provides an interactive animation facility that uses the ProB [5] animator in the background. When executed on a given root element of an EMF resource, Meeduse is synchronised with the resource and every Eclipse tool also synchronised with the same resource is expected to be compatible with Meeduse.
In our solution, one can use our Sirius artifacts for visualizing the models (the TT and the BDD) issued from
the merging meta-model. Sirius has two bene ts: (
EMF for meta-modeling and the automatic extraction of an editor plugin in a classical MDE approach. The AtelierB prover for theorem proving in order to prove that the various B speci cations (the model construction and the model transformation) preserve the meta-model structural properties.
Meeduse was involved in order to translate an Ecore meta-model into a B speci cation, and also for debugging and executing the transformation given instance of the input meta-model.
In our approach, we are not advising that the MDE expert learns the B method and its associated tooling, or conversely that the FM expert learns meta-modeling with its tools. We believe that skills in both domains are required, and we suggest a way to make people collaborate. Meeduse provides practical solutions for that, as shown by this application. Furthermore, we exploited neither the whole MDE capabilities nor the whole FM capabilities, but we limited our proposal there to a subset of what can be done for the particular case of model-to-model transformations. From a methodological point of view we were able to de ne how formal DSL execution semantics can be applied to de ne model transformations. In general, we are satis ed with the application of Meeduse to the model-to-model transformation problem because as far as we know none of the existing works combine theorem proving and model-checking in a publicly available tool which is well-integrated within EMF-based platforms. The performance mainly depends on the performance of ProB. When the number of model elements grows exponentially (14 input ports and 4 output ports) Meeduse went out of memory. For bigger examples, it should be useful to try the experiments on a machine with higher performances than that on which we have done these measures.
For readability, we believe that the verbose notation of the B method is accessible (refer to the appendix) because it recalls some programmatic styles. It is often said to be less di cult than other formal notations. Our transformation le is about 150 lines which remains reasonable. We think that model transformation interests the safety-critical community whose main intention is to develop systems which are bug-free because a failure can lead to human loss. This study gives solutions to this problem with the support of a tool and advocates for a collaboration between MDE and FM experts. portRow(rr) == (cellPort −1 ; cells) B rr ; maxPort(pp,rr) == pp ∈ InputPort ∧ rr ⊆ Row ∧ ¬ ( ∃ ss . (ss ∈ InputPort ∧ ss 6= pp ∧ ss ∈ dom(portRow(rr))
∧ card(portRow(rr)[{ss}]) > card(portRow(rr)[{pp}]))) ; zeroCells(pp) == (cellPort −1 [{pp}] ∩ cells −1 [selectedRows]) ∩ Cell value −1 [{FALSE}] ; oneCells(pp) == (cellPort −1 [{pp}] ∩ cells −1 [selectedRows]) ∩ Cell value −1 [{TRUE}] ; selectedCells == dom(Cell selected B {TRUE}) ; outputCells(rr) == cells −1 [{rr}] ∩ cellPort −1 [OutputPort] ; inputCells(rr) == cells −1 [{rr}] ∩ cellPort −1 [InputPort]
branchOne, branchZero, seqTree, selectedPorts, treePorts, seqLink INVARIANT branchOne ⊆ Tree ∧ branchZero ⊆ Tree ∧ selectedPorts ⊆ Port ∧ treePorts ∈ InputPort ↔ Tree ∧ seqTree ∈ seq(Tree) ∧ seqLink ∈ seq(BOOL)
branchOne, branchZero, selectedPorts := ∅ , ∅ , ∅ || treePorts, seqTree, seqLink := ∅ , ∅ , ∅ || setLastTree(card(Subtree)) SELECT zeroCells(port) 6= ∅ THEN
Cells SetSelected(zeroCells(port), TRUE) || branchZero := branchZero ∪ treePorts[{port}] || seqLink := seqLink ← (FALSE) WHEN oneCells(port) 6= ∅ THEN
Cells SetSelected(oneCells(port), TRUE) || branchOne := branchOne ∪ treePorts[{port}] || seqLink := seqLink ← (TRUE)
END END; setLinks =
t1 = first(seqTree) ∧ t2 = first(tail(seqTree)) ∧ ran(seqTree) ∩ Leaf 6= ∅ ∧ card(seqTree) > 1
IF first(seqLink) = TRUE THEN Subtree SetTreeForOne(t1, t2) || seqLink := tail(seqLink)
Subtree SetTreeForZero(t1, t2) || seqLink := tail(seqLink) END || seqTree := tail(seqTree)
END; Continue =
card(seqTree) = 1 ∧ ran(seqTree) ∩ Leaf 6= ∅
seqTree := tail(seqTree) END ; Transform =
row ∈ selectedRows ∧ card(selectedRows) = 1 ∧ ∀ cc . (cc ∈ cells −1 [{row}] ∧ cellPort(cc) 6∈ OutputPort ⇒ Cell selected(cc) = TRUE)
IF card(outputCells(row)) > card(assignPort[outputCells(row)]) THEN ANY as WHERE as ∈ outputCells(row) ∧ as 6∈ Assignment THEN
Assignment NEW(as, cellPort(as), Cell value(as))
END
seqTree := seqTree ← (lastTree) ; Assignments SetOwner(outputCells(row), lastTree) ; Cells Free(inputCells(row) ∪ outputCells(row)) ; selectedPorts := selectedPorts
{app | app ∈ selectedPorts ∧ treePorts(app) : (branchZero ∩ branchOne)};
The de nition clause allows to de ne some kinds of helpers (we reuse the ATL term) that calculate some formula based on the set theory and the rst order logic predicates: zeroCells(pp) == (cellPort 1 [fppg] \ cells 1 [selectedRows]) \ Cell value 1 [fFALSEg] ; oneCells(pp) == (cellPort 1 [fppg] \ cells 1 [selectedRows]) \ Cell value 1 [fTRUEg] ; selectedCells == dom(Cell selected B fTRUEg) ; outputCells(rr) == cells 1 [frrg] \ cellPort 1 [OutputPort] ; inputCells(rr) == cells 1 [frrg] \ cellPort 1 [InputPort] zeroCells applied to a port pp gives all cells with value 0 that belong to the selected rows. The row selection mechanism will be discussed while presenting the transformation rules. De nition oneCells is similar but gives cells with value 1. outputCells and inputCells applied to a row rr gives the cells that are concerned by an output or an input port.
selectedCells gives the set of cells that are consumed during the transformation.
The algorithm proposed in the TTC'2019 call for solutions suggests to nd an input port which is (ideally) de ned in all the Rows, and turn it into an inner node. We somehow applied this technique but introduced a maximality criterion. In fact our algorithm chooses the port whose set of cells is the biggest one, with respect to the selected rows.
The screen-shot of gure 3 shows that at the beginning of the transformation the only port that can be selected is port a. This is the expected result since port a establishes the maximality criterion. Note that in the initial state all rows are selected and then a has the biggest set of cells in comparison with the other ports.
The Animation view provides two possibilities for selectPort(a) because one can select the zero value or the one value. The animation of the second occurrence of selectPort(a) leads to gure 4 where cells of value one of port a are selected and a node is created in the BDD model. In fact, every time a port is selected, a node in the BDD is created. For this state, formula maxPort identi es port d as the one satisfying the maximality criterion and then the animation view gives two possible executions of selectPort(d) (for value zero and for value one).
The animation of the rst occurrence of selectPort(d) leads to the model of gure 5 where zero cells of port d are selected and an other node is created in the BDD model. In this new state four possible rules can be triggered because ports b and c are equivalent regarding the maximality criterion. Meeduse suggests then two possibilities for each of selectPort(b) and selectPort(c). Running the second occurrence of selectPort(b) produces gure 6 from which it is possible to trigger nally rule selectPort(c) and hence reach the end of the selection step with nodes extraction.
From step of gure 6 the execution of the second occurrence of selectPort(c) leads to gure 7 where only one row r 9 has all its cells selected. Now, only rule Transform(r 9) is proposed. When applied this rule iterates several times on row r 9 until it transforms it entirely. The rst calls transform non-deterministically the row output cells into assignments with the same values ( gure 8). After consuming all output cells (in this case we have only one output cell), this rule creates a Leaf and then removes the row from the model together with its cells. By this way row r 9 and its cells will not be considered for the next calculus of the enabledness conditions of the transformation rules.
In gure 9, after removing row r 9, the enabled rules are those that create links between nodes, assignments and
leafs. These are successive occurrences of operation setLinks: setLinks(
Figure 10 gives the resulting model after a row is entirely consumed and the corresponding path in the BDD is produced. Rule continue then updates the internal state of the B machine and makes possible the port selection process for the remaining rows. From the model of gure 10 only port c with value zero can be selected. Indeed, given the set of selected rows and cells, only port c satis es the maximality criterion.