基于描述邏輯ALCUQI的UML類圖元模型形式化方法

楊小鋼

（重慶郵電大學軟件工程學院，重慶 400065）

0 引言

UML類圖是一種圖形化的建模語言，雖然其表示直觀，但它卻是一種半形式化的語言，缺乏精確的形式化語義表示，難易保證建立模型語義的一致性。而且對于模型語義一致性的檢測往往是靠人工檢測，實現(xiàn)模型一致性的自動檢測是一件十分有價值的事。描述邏輯能對領域知識進行形式化的表示，同時描述邏輯還提供有相應的推理服務。本文采用基于描述邏輯的方法，研究類圖的元模型中元元素與描述邏輯間的對應關系，實現(xiàn)類圖元模型的形式化轉化。

1 描述邏輯ALCUQI

描述邏輯是一種對領域知識表示的形式化語言，適合表示關于概念與概念層次結構的知識[1]。描述邏輯語言的名稱與描述邏輯中包含的構造算子有關。AL是描述邏輯中最為基本的描述邏輯語言，任何其他的描述語言都是在AL的基礎之上擴展得到的。在AL語言當中，否定是只能被用于原子概念中，而且在角色存在變量范圍的情況下是只允許使用全局變量的[2]。

描述邏輯ALCUQI的語法和語義：

描述邏輯ALCUQI是在AL的基礎擴展到角色逆算子和有限制的數(shù)量約束算子得來的。

定義令A為原子概念，?為全概念，⊥為空概念，C為復合概念，NC是概念名集合，NR為角色集合，NO為個體名集合則ALCUQI的概念集合是滿足下列條件的最小集合：

1.任意概念C∈NC是ALCUQI概念。

2.任意個體名O∈NO是ALCUQI概念。

3.若 C，D∈NC，D∈NC，R∈NR，則都是ALCUQI概念。

表1 ALCUQI的語法及語義表

2 UML類圖元模型形式化

2.1類圖元模型形式化背景及思路

本節(jié)首先介紹類圖元模型的形式化背景，介紹元對象機制MOF，分析模型與元模型間的對應關系，然后介紹本文進行類圖元模型形式化的思路。

（1）類圖元模型的形式化背景

模型是模型驅動開發(fā)過程中的核心，是對客觀世界中事物的抽象，也是事物傳遞的信息的載體。元模型是描述模型的模型，可以將元模型看作是描述模型的一種語言。元對象機制MOF是國際對象組織OMG提出的一種對元模型進行描述的規(guī)范的公共抽象定義語言。MOF將元模型的體系結構分為4層：M0信息層、M1模型層、M2元模型、M3元元模型層，四層之間的關系[3]。如圖1所示。

圖1 MOF體系結構

從模型層面來看，人們使用模型對客觀世界中存在的事物進行描述，使用元模型對模型進行描述，使用元元模型對元模型進行描述。多個模型可以由一個元模型來描述，多個元模型可以由一個元元模型來描述。例如模型可以看作是元模型的實例化結果，元模型是對模型的抽象分類。

從元素層面來看，模型是由一個或者多個元素組成，元模型是由一個或者多個元元素組成，元元模型是由一個或者多個元元元素組成。如圖2所示。

圖2 模型及元素組織結構

使用元模型對模型進行描述實際上就是使用元模型中的元元素對模型中的元素進行描述，元素是元元素的實例化結果，元元素是對元素的抽象分類，既是用元元素建模的結果得到元素。元元素與元元元素之間關系亦然。因此，使用元模型對模型進行描述實際就是將元模型中的元元素實例化為模型中的元素。使用元元模型對元模型進行描述實際上就是將元元模型中的元元元素實例化為元模型中的元元素。

（2）類圖元模型的形式化思路

從圖3中可以看出多維數(shù)據(jù)模型是在MOF的M1模型層，多維數(shù)據(jù)元模型在MOF的M2元模型層。多維數(shù)據(jù)模型和多維數(shù)據(jù)元模型的關系與模型和元模型的關系相同，多維數(shù)據(jù)元模型用來描述多維數(shù)據(jù)模型，多維數(shù)據(jù)模型是多維數(shù)據(jù)元模型的實例化結果。多維數(shù)據(jù)元模型是多維數(shù)據(jù)模型的元模型，多維數(shù)據(jù)元模型是將多維所具有的特點如事實、維、級別、層次、度量等元素按照類圖的關聯(lián)約束進行組織的。多維數(shù)據(jù)模型的知識表示與類圖不同，多維數(shù)據(jù)模型的組成元素是由復雜的對象構成，若直接對多維數(shù)據(jù)模型中的組成元素表示為描述邏輯中的概念或者角色，就會造成語義的缺失[4]。

圖3 關系數(shù)據(jù)模型與多維數(shù)據(jù)模型之間的關聯(lián)

為了解決使用描述邏輯直接表示多維數(shù)據(jù)模型存在的問題，本文使用多維數(shù)據(jù)元模型表示出多維數(shù)據(jù)模型，使用類圖元模型表示多維數(shù)據(jù)元模型。從而間接地表示出多維數(shù)據(jù)模型。如圖4所示。

圖4 類圖元模型形式化思路

對多維數(shù)據(jù)元模型形式化，就是根據(jù)語義對多維數(shù)據(jù)元模型中的元素進行形式化。多維數(shù)據(jù)元模型繼承關系數(shù)據(jù)元模型，所以多維數(shù)據(jù)元模型中的元素是關系數(shù)據(jù)元模型中元素集合的子集。所以首先需要對關系數(shù)據(jù)模型中的元素形式化。關系數(shù)據(jù)模型中的元素是由關系數(shù)據(jù)元模型中的元元素描述，所以對關系數(shù)據(jù)模型中的元素形式化首先需要對關系數(shù)據(jù)元模型中的元元素進行形式化。

CWM中的元模型都是使用類圖進行組織的[4]，所以多維數(shù)據(jù)元模型是由類圖元模型進行描述。類圖元模型此時屬于MOF中的M3元元模型層，類圖元模型中的元元素此時就是元元元素。即多維數(shù)據(jù)元模型中的元元素由類圖元模型中的元元素進行描述。

綜上所述，對多維數(shù)據(jù)模型的形式化轉化為根據(jù)語義對組成類圖元模型的元元素進行形式化。

2.2類圖元模型形式化

UML標準文檔中給出了類圖元模型包含的所有元元素。在此本文只討論平時UML建模中設計到的類圖元模型的主要元元素Class、Property、Association、Generalization。

圖5 類圖元模型

（1）Class的形式化

面向對象的軟件開發(fā)中將類描述為一組具有共同特征的對象的集合，表明集合Class中包含的元素在某一方面具有相同的特征。類具有集合的特性。例如元元素DataType類中的對象指類包含的屬性值的數(shù)據(jù)類型。

用集合表示元元素Class的語義：

ClassI={o|o是類圖中的元元素類}

使用一階邏輯表示Class的語義：

一元謂詞：C

等同于描述邏輯ALCUQI的概念C。

（2）Attribute的形式化

UML標準文檔中將屬性的語義描述為“通過ownedAttribute與 Class相關聯(lián)的 property叫做 Attri?bute，Attribute是一個結構特征。Attribute將類的實例與Attribute類型相關聯(lián)”。

圖5中元元素Class和元元素property的組合語義表明Attribute是Class的組成元素，并且Attribute所代表的屬性值還具有特定的數(shù)據(jù)類型。通過對類圖元模型中元元素Class、Attribute和DataType三者間關聯(lián)語義的分析如圖6。

圖6 Class、Attribute和DataType三者間關聯(lián)

因此，將 Attribute作為一個集合，將 Class和DataType看作兩個集合，Attribute作為 Class和DataType兩個集合元素所構成的笛卡爾集。

用集合表示元元素Attribute的語義：

使用一階邏輯表示Attribute與Class、DataType之間關聯(lián)的語義為：

對應的描述邏輯ALCUQI的形式化表示為：

（3）Association的形式化

圖5中元元素property和association的組合關聯(lián)中property的角色ownedend表明property是被associ?ation擁有的端，除此外，property和association的二元關聯(lián)中property的角色是成員端 memberend，表示property是association的組成成員，由于property的基數(shù)約束是2…*，即一個association擁有兩個或者prop?erty。另外，圖中可看到property與class存在組合關系，property在該關聯(lián)中是ownedAttribute角色，表示property是class的成員，根據(jù)重數(shù)可知一個property屬于一個class。所以，一個association連接兩個或多個class。根據(jù)上述整理得到類圖中association連接class的語義如圖7。

圖7 association連接class

①用集合表示元元素Association的語義：

Class1、Class2看作兩個集合，Association是兩集合元素構成的笛卡爾集。

使用一階邏輯表示Association與Class1、Class2之間關聯(lián)的語義為：

對應的描述邏輯ALCUQI的形式化表示為：

值得注意的是一般的二元關聯(lián)Association除了包含關聯(lián)名外，還擁有關聯(lián)兩端的關聯(lián)角色，并且角色是具有多重性（用[i,j]表示），表示通過關聯(lián)由多少個對象參與該關聯(lián)。

圖8 帶關聯(lián)名和角色的二元關聯(lián)

②帶角色關聯(lián)的重數(shù)約束

圖8中通過關聯(lián)Association（關聯(lián)名為Associa?tion）連接的Class1對象的角色是Class1且重數(shù)約束是0…1。Class1、Class2看作兩個集合，Association是兩集合元素構成的笛卡爾集（xi表示Class1的元素，yi表示Class2的元素，（xi,yi）代表集合class1，（yi,xi）代表集合class2，class1∪class2=Association）。

使用一階邏輯表示是上述語義：

圖8中通過關聯(lián)Association連接的Class2對象的角色是class2且重數(shù)約束是0…1。Class1、Class2看作兩個集合，Association是兩集合元素構成的笛卡爾集（xi表示Class1的元素，yi表示Class2的元素，（xi,yi）代表集合Class1，（yi,xi）代表集合class2，class1∪class2=Association）。

使用一階邏輯表示是上述語義：對應的描述邏輯ALCUQI的形式化表示為：

（4）Aggregation的形式化

在UML建模中將關聯(lián)細分為一般二元關聯(lián)、聚合關聯(lián)、組合關聯(lián)。從圖5類圖元模型中可以看出元元素Association通過和元元素Type的關聯(lián)來指定關聯(lián)的類型。結合2.2.3小節(jié)中一般二元關聯(lián)的描述歸納得到聚合的關聯(lián)關系如圖9。

圖9 關聯(lián)與類型

二元關聯(lián)中有一種特殊形式是聚集，也稱聚合，表示整體與部分之間的關系。整體一端用一個實心的菱形箭頭表示。表示各部分的生命周期獨立于整體，而且一個部分可同時屬于多個整體[8]。如圖10元元素Class1由Class2聚合而成，Class1消失后Class2也可獨立存在（此處聚合關聯(lián)的關聯(lián)名為Aggregation）。

圖10 聚合關聯(lián)

用集合表示元元素Aggregation的語義：

使用一階邏輯表示Aggregation與Class1、Class2之間關聯(lián)的語義為：

對應的描述邏輯ALCUQI的形式化表示為：

（5）Composition的形式化

組合是聚合的強關聯(lián)形式，比聚合多了2個約束，第一個約束是部件實例只能同時包含在至多1個組合實例中，這就要求組合管理端重數(shù)的上邊界不能大于1；第二個約束是強調(diào)部件具有與組合相同的生命周期[4]。組合如圖11，元元素Class1由Class2組合而成，一旦Class1消失Class2隨之消失（此處聚合關聯(lián)的關聯(lián)名為 Composition）。

圖11 組合關聯(lián)

用集合表示元元素Composition的語義：

使用一階邏輯表示Composition與Class1、Class2之間關聯(lián)的語義為：

對應的描述邏輯ALCUQI的形式化表示為：

（6）Generalization的形式化

圖5類圖元模型中元元素Class自身存在自關聯(lián)，自關聯(lián)中有superClass和class兩端，superClass代表超類即父類，class端代表子類。用集合論術語來說，超類對象是一個集合，其子類對象集合是它的一個子集合[8]。用泛化關系可組合一個有層次的概念結構。如圖5中Class繼承Classifier。

用集合表示元元素Generalization的語義：

使用一階邏輯表示Class繼承Classifier的語義為：

對應的描述邏輯ALCUQI描述形式為：

2.3類圖元模型的實例舉例

圖12是類圖元模型的實例舉例，描述的是題庫系統(tǒng)中教師出題的場景，一個教師屬于一個學院，教師和學院之間存在聚合關聯(lián)，教師作為出題人出考試題，一個教師可以出多個試題，教師和試題間存在出題的二元關聯(lián)，試題和答案選項之間存在組合管理，一個試題包含多個答案選項，教師繼承系統(tǒng)中用戶的一部分功能。

圖12 教師出題

根據(jù)2.2節(jié)中類圖元模型的形式化方法，圖12教師出題實例在描述邏輯ALCUQI的描述邏輯表示如下：

3 正確性證明

通過上述分析可知，類圖元模型的元元素與描述邏輯ALCUQI具有對應關系，類圖元模型的元元素可以轉化為描述邏輯ALCUQI的知識庫。描述邏輯AL?CUQI知識庫KB包含Tbox和Abox。Tbox引入應用領域中的術語表（terminology）；Abox包含對個體的實例斷言（instance assertion）和關系斷言（role assertion）。此外描述邏輯還提供了推理服務[1]。描述邏輯ALCUQI的解釋I=(△I,.I)，其中，△I是解釋論域；.I是解釋函數(shù)。如果解釋I=(△I,.I)滿足知識庫KB中的所有斷言，則I是KB的一個模型。如果知識庫KB存在一個模型，則KB 是可滿足的。對于知識庫中的一個概念C，如果存在一個KB的一個模型I則稱概念C是可滿足的[9]。

類圖元模型元元素與描述邏輯ALCUQI知識庫間的轉化可以通過設計一個函數(shù)f來實現(xiàn)。轉化函數(shù)f的正確性證明如下：

假設M是類圖元模型的一個模型，f（M）是轉化后的描述邏輯ALCUQI的知識庫。由于類圖元模型M的元元素的語義可以轉化為一階謂詞邏輯FOL，表示元元素能轉化為一階謂詞邏輯公式集合，因此轉化過程的正確性證明只要對于任意解釋I，I滿足M轉化得到的一階邏輯公式集合FOL（M），當且僅當I滿足轉化得到的ALCUQI知識庫f（M）。

接下來對類Class的數(shù)據(jù)類型為DataType的屬性Attribute進行討論（類圖元模型其他元素轉化證明同理可證）。類Class有屬性對應的一階邏輯謂詞表示：ClassI?{x∈△I|?y：(x,y)∈AttributeI→y∈DataTypeI} ，對應的描述邏輯ALCUQI描述形式化表示為：Class??Attribute.DataType，其對應的描述邏輯ALCUQI知識庫表示為給定M的一個模型實例I，即I是FOL（M）的模型，對任意的即對因 此 ，I是的一個模型。反之，給定 f（M）的一個模型，對應任意的，即對 Class（x），有因此，I是一階邏輯公式個模型，證明完畢。

4 結語

類圖元模型元元素能轉換為描述邏輯ALCUQI知識庫KB，可以利用支持描述邏輯ALCUQI的推理機RacerPro進行知識可滿足性的推理，實現(xiàn)類圖元模型實例化后模型的一致性檢測。本文提出的基于描述邏輯ALCUQI的類圖元模型形式化方法為UML模型形式化和一致性自動檢測的研究提供了參考價值。