形式化关系型模型转换方法的一些观点

本文主要分析了 Michael Wahler 的博士论文研究计划书 [1] ，他是 IBM Zurich 研究室的一名走读博士。他的导师是 David Basin 。他的研究题目是关系型模型转换方法的形式化。我将其中有意义的部分摘录出来。并加上了一些自己的想法和观点。这份计划书是 2004 年写的，其中一些想法和观点今天看来也不失偏颇。

今天又搜索了一下 Michael Wahler 的论文，发现他除了这一篇以外，没有以第一作者的身份发表论文。很是遗憾，他的博士论文计划书做得很好，为什么没有成果出来呢？

（蓝色部分是自己的观点和评论。）

Background and Definitions

在第一部分 Background and Definitions 中，给出了四个概念 Model 、 Transformation 、 Consistency between Models 、 Reconciliation 。这些概念和其它地方的概念有一些区别，解释如下：

Model ：   A model is a representation of a part of the function, structure and/or behavior of an application or system. A representation is said to be formal when it is based on a language that has a well-defined form (”syntax”), meaning (”semantics”), and possibly rules of analysis, inference, or proof for its constructs. The syntax may be graphical or textual.

模型是一个应用程序或者系统的功能，结构或者行为部分的一种表达方式。当一种表达方式基于一种含有良构的形式（语法），含义（语义），以及关于分析、推论或者证明其构造的规则的语言时，这种表达方式被称为形式化的。其语法可以是图形的或者是文本的。

事实上，目前对于软件模型的形式化表达，例如类图的形式化表达还是没有一个统一的标准或者语言。

Transformation ：

Functional View ： A transformation is a function that maps a tuple of models from one or more

domains onto another tuple of models in the same or different domains.

Operational View ： A transformation is a terminating algorithm that applies structural and/or

semantic changes to a model or a set of models.

对于模型转换有两种观点：

功能的观点：一个转换是一个函数，它可以将一组模型从一个或者更多的领域映射到相同或者不同领域中的另一组模型。

操作的观点：一个转换是一个可停机算法，它将结构或者语义的变化应用到一个或者一组模型。

描述性（ declarative ）的模型转换语言就是基于功能的观点；而命令性（ imperative ）的模型转换语言则是基于操作的观点。

 

Consistency between models ：

A set of models is consistent with respect to a consistency concept if the models fulfill the syntactic consistency conditions and the semantics of the models fulfills the semantic consistency conditions of the consistency concept.

模型一致性：如果一组模型符合语法一致性条件并且其语义符合某种一致性概念下的语义一致性条件，则这组模型对于这种一致性概念是一致的。

简单的理解：如果一组模型符合某种语法和语义的规则，则认为它们对于这组规则是一致的，也就是规则是成立的。最简单的语法一致性规则是， UML 类图的构建规则，例如类可以包含属性，但是属性不能包含类。如果一个 UML 模型中属性包含了类，则此模型不是良构的，破坏了 UML 语法一致性规则。

Reconciliation ：

Reconciliation is the process of making inconsistent models consistent according to a consistency concept and the intent and expectation of the user. Depending on its requirements, the reconciliation process may run automatically or interactively.

消解（冲突消解）：消解是一种过程，其目的是为了将不一致的模型根据一致性概念和用户的决定和希望重新变为一致。根据其要求的不同，消解过程可以自动运行或者交互的运行。

消解实际上就是模型转换过程，对于一组模型转换规则，如果源模型和目标模型是一致的，则它们符合规则，不需要转换。如果不符合规则，则需要消解 / 转换，通过将它们变为一致的过程（通常是对目标模型进行增、删、改）达到模型转换的目的。消解以后的模型则具有了一致性。

这种方法在 MTF （ IBM 的模型转换工具）中实现了。

Running Example

第二部分给出了一个模型转换的实例如下：

然后给出了一个关系型的模型转换代码（可以看出，这就是 MTF 的代码）：

当然，文中给出的代码是不完整的，可能作者不想牵扯到太多 MTF 的细节，毕竟这是一个博士开题报告，在没有对所有的关系型模型转换语言进行分析之前，就使用 MTF ，也是不恰当的。因此他还给出了基于一阶逻辑的转换定义：

一阶逻辑用来表示模型转换的语义是足够的， OCL 语言其实是一阶逻辑的另一种表现形式，所以有一些研究者将 OCL 做为模型转换语言。其实一阶逻辑看起来还是很清爽的，比具体的模型转换代码更好理解。

Related Work

相关工作包括 MDA 、业务过程集成与自动化（ Business Process Integration and Automation ）、形式化语言的语法和语义、数据库修订理论（ Database Revision Theory ）

其中业务过程集成与自动化不太了解，数据库修订理论是和人工智能领域相关的，也不太理解。

State of the Art

这一节介绍目前模型转换的研究现状。一共有三点内容：第一介绍了模型转换技术出现的动机；第二部分介绍了模型转换技术的分类，分类方法来自 [2] ；第三部分介绍了目前的关系型模型转换方法，其中最著名的是 [3] ，他第一次使用集合论中的关系来表示元模型间的转换规则。

Open Questions and Tasks

这是本文最有意义的一节了，其中介绍了关系型模型转换语言形式化领域中的两个 open question 。

1. The syntax and semantics of the expression language that is used to formulate the set comprehension predicate has to be defined and its logical properties have to be proved. As one single language will not be sufficient for the several use cases for transformations, several languages which map to distinct logical classes have to be investigated.

用来阐明集合理解断言（ set comprehension predicate ，用来表达模型转换规则的关系往往使用集合理解断言来定义）的语言的语法和语义必须被定义好，它的逻辑属性也必须验证。因为单一的语言不足以表达模型转换中的各种使用案例，所以必须研究多种语言，它们分别映射到不同的逻辑类型。

总的来说，作者希望通过研究不同的语言来找到适合描述模型转换规则的关系型语言，或者自己定义这种语言的语法和语义。这些语言都应该是基于某种逻辑的。

2. An execution semantics needs to be defined for relations in the model transformation context. The semantics needs to support two mechanisms:

(a) Two or more models have to be checked for consistency, i.e., that they form a valid tuple with respect to a relation that was defined on them.

(b) Reconciliation has to be supported to be able to ”repair” models that are inconsistent with respect to a relation.

在模型转换环境中，必须定义关系的可执行语义。这种语义必须支持以下两种机制：

(a)    两个或者更多的模型必须能够进行一致性检查。例如，根据定义在它们之上的一个关系来检查他们是否构成了一个有效的组合。

(b)    如果模型不符合一个关系定义的一致性，则必须有一个消解机制来“修复”模型。

作者希望能够定义一个基于关系的可执行语义，这个语义有两种功能：一是检查模型之间是否能够保持一致性，这里的一致性使用关系来定义，即用关系定义的模型转换规则；二是当模型不一致时，是否可以使用消解机制来修复模型从而重新达到一致。这里的消解机制相当于模型转换的执行机制。而消解的过程就是模型转换的执行过程。

理想的关系型模型转换语言的重要特征

在这一节作者还列举了关系型模型转换语言应该具有的某些重要特征，主要包括：

Termination （可停机性）：模型转换方法应该保证是可以停机的，不能包含死循环等。

Confluence （汇合？）：关系的执行顺序是否对模型转换的结果造成影响？在关系之间是否存在着显式、隐式的控制流？两个关系的域并行执行并且有交集时，是否会导致问题？

一般的关系型模型转换语言的执行顺序是隐式的被定义的，例如 MTF ，它从第一个可以执行的 relate 语句开始，然后在语句中调用其它子语句。在 QVT 草案 [4] 中， Relation 语言将所有的 top Relation 语句依次执行，然后在语句中调用其它子语句。而在其它的一些模型转换语言中例如 ATL ，则类似于一般的面向对象语言，是显式定义执行顺序的。

Composition （组合）：将关系组合起来时是否会导致问题？当然，由于关系是描述性的，所以它是没有副作用的，因此组合关系应当是没有问题的。但是这一点如何证明？

OCL 也是描述性的语言，它最大的特点就是无副作用，并且它的计算都被认为是原子的，不存在并行和多线程等问题。但是如何证明关系的组合不会带来副作用还真是没有人想过。

Correctness / Decidability （正确性 / 可判定性）：如何处理转换规范中可能存在的矛盾。集合理解断言可能会含有一些矛盾，它们应该可以被静态的检测出来。

Multi-Directionality （多向性）：转换是否能够被双向的执行，并且不丢失信息。双向转换要求关系必须是一个双射（ bijective ），对于某个语言，一个关系的双射性质能否静态的计算出来？

In-Place Transformations （内置转换（这个词是我发明的，哈哈！））：内置转换能否使用数学关系的方式表达出来？它可能会需要一个状态的概念，一个关系型语言如何支持这种状态的概念？

内置转换也被称为模型进化，意思就是源模型与目标模型是同一个模型。当执行这种转换时显然要复杂一些，因为规则执行的时候是互相影响的，当某一条规则执行时，也许破坏了前面规则定义的一致性。所以可能会需要一个状态来描述模型元素或者规则的执行情况。目前内置转换的研究不多。

Usability （可用性）：一个模型转换语言是否能够适应多种不同类型的转换？即使是很简单的转换规则，使用关系来表述也许是冗长的。语言能否提供一些语法上的简化机制？

目前看来，全部符合以上七点的关系型模型转换语言还没有出现， QVT 的规范 [4] 已经出台，我认为它解决了 Confluence 、 Composition 、 Correctness/Decidability 、 Muti-Directionality 和 Usability 。没有涉及到 Termination 和 In-Place Transformations 。另外，它也没有对这些性质做相关的证明。

总结

这篇文章的最大贡献就是提出了那两个 open question 。并进行了相关的分析。提炼如下：

第一个问题是：如何定义或者选择一个适于表达模型转换规则的关系型语言？它是以某种形式化逻辑做为基础的，并且具有上述的七个特性。

第二个问题是：如果定义这种关系型模型转换语言的执行语义？这里分为两个子问题，第一是如何检测模型之间的不一致性；第二是如何使用消解机制来修复模型。

从去年年底开始使用 EndNote 来管理参考文献了，这个东东真的不错啊。现在随手加参考文献的感觉真是爽！

[1]           Wahler, Michael. Formalizing Relational Model Transformation Approaches. Zurich, 2004

[2]           Krzysztof Czarnecki, Simon Helsen. Classification of Model Transformation Approaches. In: Proceedings of the 18th International Conference, OOPSLA’2003, Workshop on Generative Techniques in the context of Model Driven Architecture. Anaheim, California, USA 2003 

[3]           Kent, David Akehurst and Stuart. A Relational Approach to Defining Transformations in a Metamodel. In: H. Hussmann J.-M. Jézéquel, S. Cook (Eds.). UML 2002 - The Unified Modeling Language 5th International Conference. Dresden, Germany: Springer-Verlag 2002 LNCS 2460.243-258

[4]           OMG, MOF QVT Final Adopted Specification. 2005.