Information Technology Reference
In-Depth Information
transformation rule of the model transformation Mt is represented as a logical
formula of
form stating that for every model element satisfying a certain
(pre-)condition, there exists a target model element which stands in the relation
specified by the transformation rule with the source model element ( TRule ).
The correctness of the model transformation is stated by a formula.
∀∃
Ma:MMa. (Pre(Ma) →∀ Mb:MMb. (TRules(Ma,Mb) Post(Ma,Mb)))
where Pre is a translation of the source invariants, TRules is the conjunction
of the transformation rules, and Post is a translation of the target invariants
plus any other desired property to be proved. A proof of this formula ensures
that the transformation rules satisfy the target invariants as well as the desired
properties.
The translation into Coq of the KM3 metamodels can be performed fully
automatically. On the other hand, at the moment the verifiers have to deal
with: references in the metamodels that must be “cut” to avoid circularity in
an optimal way, the translation of the OCL invariants -which can at a large
measure be done automatically- and the translation of the ATL transformation
rules and helpers. Then he can proceed to perform the formal verification.
As a proof of concepts, we have applied our approach to a simplified version
of the well-known Class to Relational model transformation broadly studied in
the literature [19]. The resulting Coq code can be found in [20].
With this approach we lose full automation to gain in return strength of the
achieved results. We think the approach could be particularly helpful in proving
the existence of zero-fault model transformations within the development of
critical systems.
So far the non-automatic parts of the process of translation involved in our
proposal can in general be carried out directly enough to indeed provide increased
confidence in the outcome.
We are currently working on setting up a semantics of transformation lan-
guages in type theory which will lead to a greater automatical capability at the
level of the framework, particularly concerning the outlined method for trans-
lating transformations.
Our medium-term goals are the full development of the framework and its
integration with ATL and Coq. In the long-term we will work on simplifying
the proof process. In this direction we aim at generating auxiliary libraries with
proofs of basic properties and also work on proof patterns detection in order to
improve the facility of use of the proof assistant.
Acknowledgement
This work has been partially funded by the National Research and Innovation
Agency (ANII) of Uruguay through the “Verification of UML Based Behavioral
Model Transformations” project [20].
 
Search WWH ::




Custom Search