形式化關(guān)系型模型轉(zhuǎn)換方法的一些觀點(diǎn)

本文主要分析了 Michael Wahler 的博士論文研究計(jì)劃書 [1] ，他是 IBM Zurich 研究室的一名走讀博士。他的導(dǎo)師是 David Basin 。他的研究題目是關(guān)系型模型轉(zhuǎn)換方法的形式化。我將其中有意義的部分摘錄出來(lái)。并加上了一些自己的想法和觀點(diǎn)。這份計(jì)劃書是 2004 年寫的，其中一些想法和觀點(diǎn)今天看來(lái)也不失偏頗。

今天又搜索了一下 Michael Wahler 的論文，發(fā)現(xiàn)他除了這一篇以外，沒有以第一作者的身份發(fā)表論文。很是遺憾，他的博士論文計(jì)劃書做得很好，為什么沒有成果出來(lái)呢？

（藍(lán)色部分是自己的觀點(diǎn)和評(píng)論。）

Background and Definitions

在第一部分 Background and Definitions 中，給出了四個(gè)概念 Model 、 Transformation 、 Consistency between Models 、 Reconciliation 。這些概念和其它地方的概念有一些區(qū)別，解釋如下：

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.

模型是一個(gè)應(yīng)用程序或者系統(tǒng)的功能，結(jié)構(gòu)或者行為部分的一種表達(dá)方式。當(dāng)一種表達(dá)方式基于一種含有良構(gòu)的形式（語(yǔ)法），含義（語(yǔ)義），以及關(guān)于分析、推論或者證明其構(gòu)造的規(guī)則的語(yǔ)言時(shí)，這種表達(dá)方式被稱為形式化的。其語(yǔ)法可以是圖形的或者是文本的。

事實(shí)上，目前對(duì)于軟件模型的形式化表達(dá)，例如類圖的形式化表達(dá)還是沒有一個(gè)統(tǒng)一的標(biāo)準(zhǔn)或者語(yǔ)言。

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.

對(duì)于模型轉(zhuǎn)換有兩種觀點(diǎn)：

功能的觀點(diǎn)：一個(gè)轉(zhuǎn)換是一個(gè)函數(shù)，它可以將一組模型從一個(gè)或者更多的領(lǐng)域映射到相同或者不同領(lǐng)域中的另一組模型。

操作的觀點(diǎn)：一個(gè)轉(zhuǎn)換是一個(gè)可停機(jī)算法，它將結(jié)構(gòu)或者語(yǔ)義的變化應(yīng)用到一個(gè)或者一組模型。

描述性（ declarative ）的模型轉(zhuǎn)換語(yǔ)言就是基于功能的觀點(diǎn)；而命令性（ imperative ）的模型轉(zhuǎn)換語(yǔ)言則是基于操作的觀點(diǎn)。

?

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.

模型一致性：如果一組模型符合語(yǔ)法一致性條件并且其語(yǔ)義符合某種一致性概念下的語(yǔ)義一致性條件，則這組模型對(duì)于這種一致性概念是一致的。

簡(jiǎn)單的理解：如果一組模型符合某種語(yǔ)法和語(yǔ)義的規(guī)則，則認(rèn)為它們對(duì)于這組規(guī)則是一致的，也就是規(guī)則是成立的。最簡(jiǎn)單的語(yǔ)法一致性規(guī)則是， UML 類圖的構(gòu)建規(guī)則，例如類可以包含屬性，但是屬性不能包含類。如果一個(gè) UML 模型中屬性包含了類，則此模型不是良構(gòu)的，破壞了 UML 語(yǔ)法一致性規(guī)則。

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.

消解（沖突消解）：消解是一種過(guò)程，其目的是為了將不一致的模型根據(jù)一致性概念和用戶的決定和希望重新變?yōu)橐恢隆８鶕?jù)其要求的不同，消解過(guò)程可以自動(dòng)運(yùn)行或者交互的運(yùn)行。

消解實(shí)際上就是模型轉(zhuǎn)換過(guò)程，對(duì)于一組模型轉(zhuǎn)換規(guī)則，如果源模型和目標(biāo)模型是一致的，則它們符合規(guī)則，不需要轉(zhuǎn)換。如果不符合規(guī)則，則需要消解 / 轉(zhuǎn)換，通過(guò)將它們變?yōu)橐恢碌倪^(guò)程（通常是對(duì)目標(biāo)模型進(jìn)行增、刪、改）達(dá)到模型轉(zhuǎn)換的目的。消解以后的模型則具有了一致性。

這種方法在 MTF （ IBM 的模型轉(zhuǎn)換工具）中實(shí)現(xiàn)了。

Running Example

第二部分給出了一個(gè)模型轉(zhuǎn)換的實(shí)例如下：

然后給出了一個(gè)關(guān)系型的模型轉(zhuǎn)換代碼（可以看出，這就是 MTF 的代碼）：

當(dāng)然，文中給出的代碼是不完整的，可能作者不想牽扯到太多 MTF 的細(xì)節(jié)，畢竟這是一個(gè)博士開題報(bào)告，在沒有對(duì)所有的關(guān)系型模型轉(zhuǎn)換語(yǔ)言進(jìn)行分析之前，就使用 MTF ，也是不恰當(dāng)?shù)摹Ｒ虼怂€給出了基于一階邏輯的轉(zhuǎn)換定義：

一階邏輯用來(lái)表示模型轉(zhuǎn)換的語(yǔ)義是足夠的， OCL 語(yǔ)言其實(shí)是一階邏輯的另一種表現(xiàn)形式，所以有一些研究者將 OCL 做為模型轉(zhuǎn)換語(yǔ)言。其實(shí)一階邏輯看起來(lái)還是很清爽的，比具體的模型轉(zhuǎn)換代碼更好理解。

Related Work

相關(guān)工作包括 MDA 、業(yè)務(wù)過(guò)程集成與自動(dòng)化（ Business Process Integration and Automation ）、形式化語(yǔ)言的語(yǔ)法和語(yǔ)義、數(shù)據(jù)庫(kù)修訂理論（ Database Revision Theory ）

其中業(yè)務(wù)過(guò)程集成與自動(dòng)化不太了解，數(shù)據(jù)庫(kù)修訂理論是和人工智能領(lǐng)域相關(guān)的，也不太理解。

State of the Art

這一節(jié)介紹目前模型轉(zhuǎn)換的研究現(xiàn)狀。一共有三點(diǎn)內(nèi)容：第一介紹了模型轉(zhuǎn)換技術(shù)出現(xiàn)的動(dòng)機(jī)；第二部分介紹了模型轉(zhuǎn)換技術(shù)的分類，分類方法來(lái)自 [2] ；第三部分介紹了目前的關(guān)系型模型轉(zhuǎn)換方法，其中最著名的是 [3] ，他第一次使用集合論中的關(guān)系來(lái)表示元模型間的轉(zhuǎn)換規(guī)則。

Open Questions and Tasks

這是本文最有意義的一節(jié)了，其中介紹了關(guān)系型模型轉(zhuǎn)換語(yǔ)言形式化領(lǐng)域中的兩個(gè) 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.

用來(lái)闡明集合理解斷言（ set comprehension predicate ，用來(lái)表達(dá)模型轉(zhuǎn)換規(guī)則的關(guān)系往往使用集合理解斷言來(lái)定義）的語(yǔ)言的語(yǔ)法和語(yǔ)義必須被定義好，它的邏輯屬性也必須驗(yàn)證。因?yàn)閱我坏恼Z(yǔ)言不足以表達(dá)模型轉(zhuǎn)換中的各種使用案例，所以必須研究多種語(yǔ)言，它們分別映射到不同的邏輯類型。

總的來(lái)說(shuō)，作者希望通過(guò)研究不同的語(yǔ)言來(lái)找到適合描述模型轉(zhuǎn)換規(guī)則的關(guān)系型語(yǔ)言，或者自己定義這種語(yǔ)言的語(yǔ)法和語(yǔ)義。這些語(yǔ)言都應(yīng)該是基于某種邏輯的。

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.

在模型轉(zhuǎn)換環(huán)境中，必須定義關(guān)系的可執(zhí)行語(yǔ)義。這種語(yǔ)義必須支持以下兩種機(jī)制：

(a)??? 兩個(gè)或者更多的模型必須能夠進(jìn)行一致性檢查。例如，根據(jù)定義在它們之上的一個(gè)關(guān)系來(lái)檢查他們是否構(gòu)成了一個(gè)有效的組合。

(b)??? 如果模型不符合一個(gè)關(guān)系定義的一致性，則必須有一個(gè)消解機(jī)制來(lái)“修復(fù)”模型。

作者希望能夠定義一個(gè)基于關(guān)系的可執(zhí)行語(yǔ)義，這個(gè)語(yǔ)義有兩種功能：一是檢查模型之間是否能夠保持一致性，這里的一致性使用關(guān)系來(lái)定義，即用關(guān)系定義的模型轉(zhuǎn)換規(guī)則；二是當(dāng)模型不一致時(shí)，是否可以使用消解機(jī)制來(lái)修復(fù)模型從而重新達(dá)到一致。這里的消解機(jī)制相當(dāng)于模型轉(zhuǎn)換的執(zhí)行機(jī)制。而消解的過(guò)程就是模型轉(zhuǎn)換的執(zhí)行過(guò)程。

理想的關(guān)系型模型轉(zhuǎn)換語(yǔ)言的重要特征

在這一節(jié)作者還列舉了關(guān)系型模型轉(zhuǎn)換語(yǔ)言應(yīng)該具有的某些重要特征，主要包括：

Termination （可停機(jī)性）：模型轉(zhuǎn)換方法應(yīng)該保證是可以停機(jī)的，不能包含死循環(huán)等。

Confluence （匯合？）：關(guān)系的執(zhí)行順序是否對(duì)模型轉(zhuǎn)換的結(jié)果造成影響？在關(guān)系之間是否存在著顯式、隱式的控制流？?jī)蓚€(gè)關(guān)系的域并行執(zhí)行并且有交集時(shí)，是否會(huì)導(dǎo)致問題？

一般的關(guān)系型模型轉(zhuǎn)換語(yǔ)言的執(zhí)行順序是隱式的被定義的，例如 MTF ，它從第一個(gè)可以執(zhí)行的 relate 語(yǔ)句開始，然后在語(yǔ)句中調(diào)用其它子語(yǔ)句。在 QVT 草案 [4] 中， Relation 語(yǔ)言將所有的 top Relation 語(yǔ)句依次執(zhí)行，然后在語(yǔ)句中調(diào)用其它子語(yǔ)句。而在其它的一些模型轉(zhuǎn)換語(yǔ)言中例如 ATL ，則類似于一般的面向?qū)ο笳Z(yǔ)言，是顯式定義執(zhí)行順序的。

Composition （組合）：將關(guān)系組合起來(lái)時(shí)是否會(huì)導(dǎo)致問題？當(dāng)然，由于關(guān)系是描述性的，所以它是沒有副作用的，因此組合關(guān)系應(yīng)當(dāng)是沒有問題的。但是這一點(diǎn)如何證明？

OCL 也是描述性的語(yǔ)言，它最大的特點(diǎn)就是無(wú)副作用，并且它的計(jì)算都被認(rèn)為是原子的，不存在并行和多線程等問題。但是如何證明關(guān)系的組合不會(huì)帶來(lái)副作用還真是沒有人想過(guò)。

Correctness / Decidability （正確性 / 可判定性）：如何處理轉(zhuǎn)換規(guī)范中可能存在的矛盾。集合理解斷言可能會(huì)含有一些矛盾，它們應(yīng)該可以被靜態(tài)的檢測(cè)出來(lái)。

Multi-Directionality （多向性）：轉(zhuǎn)換是否能夠被雙向的執(zhí)行，并且不丟失信息。雙向轉(zhuǎn)換要求關(guān)系必須是一個(gè)雙射（ bijective ），對(duì)于某個(gè)語(yǔ)言，一個(gè)關(guān)系的雙射性質(zhì)能否靜態(tài)的計(jì)算出來(lái)？

In-Place Transformations （內(nèi)置轉(zhuǎn)換（這個(gè)詞是我發(fā)明的，哈哈！））：內(nèi)置轉(zhuǎn)換能否使用數(shù)學(xué)關(guān)系的方式表達(dá)出來(lái)？它可能會(huì)需要一個(gè)狀態(tài)的概念，一個(gè)關(guān)系型語(yǔ)言如何支持這種狀態(tài)的概念？

內(nèi)置轉(zhuǎn)換也被稱為模型進(jìn)化，意思就是源模型與目標(biāo)模型是同一個(gè)模型。當(dāng)執(zhí)行這種轉(zhuǎn)換時(shí)顯然要復(fù)雜一些，因?yàn)橐?guī)則執(zhí)行的時(shí)候是互相影響的，當(dāng)某一條規(guī)則執(zhí)行時(shí)，也許破壞了前面規(guī)則定義的一致性。所以可能會(huì)需要一個(gè)狀態(tài)來(lái)描述模型元素或者規(guī)則的執(zhí)行情況。目前內(nèi)置轉(zhuǎn)換的研究不多。

Usability （可用性）：一個(gè)模型轉(zhuǎn)換語(yǔ)言是否能夠適應(yīng)多種不同類型的轉(zhuǎn)換？即使是很簡(jiǎn)單的轉(zhuǎn)換規(guī)則，使用關(guān)系來(lái)表述也許是冗長(zhǎng)的。語(yǔ)言能否提供一些語(yǔ)法上的簡(jiǎn)化機(jī)制？

目前看來(lái)，全部符合以上七點(diǎn)的關(guān)系型模型轉(zhuǎn)換語(yǔ)言還沒有出現(xiàn)， QVT 的規(guī)范 [4] 已經(jīng)出臺(tái)，我認(rèn)為它解決了 Confluence 、 Composition 、 Correctness/Decidability 、 Muti-Directionality 和 Usability 。沒有涉及到 Termination 和 In-Place Transformations 。另外，它也沒有對(duì)這些性質(zhì)做相關(guān)的證明。

總結(jié)

這篇文章的最大貢獻(xiàn)就是提出了那兩個(gè) open question 。并進(jìn)行了相關(guān)的分析。提煉如下：

第一個(gè)問題是：如何定義或者選擇一個(gè)適于表達(dá)模型轉(zhuǎn)換規(guī)則的關(guān)系型語(yǔ)言？它是以某種形式化邏輯做為基礎(chǔ)的，并且具有上述的七個(gè)特性。

第二個(gè)問題是：如果定義這種關(guān)系型模型轉(zhuǎn)換語(yǔ)言的執(zhí)行語(yǔ)義？這里分為兩個(gè)子問題，第一是如何檢測(cè)模型之間的不一致性；第二是如何使用消解機(jī)制來(lái)修復(fù)模型。

從去年年底開始使用 EndNote 來(lái)管理參考文獻(xiàn)了，這個(gè)東東真的不錯(cuò)啊。現(xiàn)在隨手加參考文獻(xiàn)的感覺真是爽！

[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.

?

?

?