形式化關系型模型轉換方法的一些觀點

本文主要分析了 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.

?

?

?