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

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

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

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

Background and Definitions

在第一部分 Background and Definitions 中，給出了四個概念 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.

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

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

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.

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

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

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

描述性（ declarative ）的模型轉(zhuǎn)換語言就是基于功能的觀點；而命令性（ imperative ）的模型轉(zhuǎ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.

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

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

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

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

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

Running Example

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

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

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

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

Related Work

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

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

State of the Art

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

Open Questions and Tasks

這是本文最有意義的一節(jié)了，其中介紹了關(guān)系型模型轉(zhuǎn)換語言形式化領(lǐng)域中的兩個 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 ，用來表達(dá)模型轉(zhuǎn)換規(guī)則的關(guān)系往往使用集合理解斷言來定義）的語言的語法和語義必須被定義好，它的邏輯屬性也必須驗證。因為單一的語言不足以表達(dá)模型轉(zhuǎn)換中的各種使用案例，所以必須研究多種語言，它們分別映射到不同的邏輯類型。

總的來說，作者希望通過研究不同的語言來找到適合描述模型轉(zhuǎn)換規(guī)則的關(guān)系型語言，或者自己定義這種語言的語法和語義。這些語言都應(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í)行語義。這種語義必須支持以下兩種機制：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

總結(jié)

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

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

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

從去年年底開始使用 EndNote 來管理參考文獻(xiàn)了，這個東東真的不錯啊。現(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.

?

?

?