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

楊小鋼

（重慶郵電大學(xué)軟件工程學(xué)院，重慶 400065）

0 引言

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

1 描述邏輯ALCUQI

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

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

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

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

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

2.任意個(gè)體名O∈NO是ALCUQI概念。

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

表1 ALCUQI的語法及語義表

2 UML類圖元模型形式化

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

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

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

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

圖1 MOF體系結(jié)構(gòu)

從模型層面來看，人們使用模型對(duì)客觀世界中存在的事物進(jìn)行描述，使用元模型對(duì)模型進(jìn)行描述，使用元元模型對(duì)元模型進(jìn)行描述。多個(gè)模型可以由一個(gè)元模型來描述，多個(gè)元模型可以由一個(gè)元元模型來描述。例如模型可以看作是元模型的實(shí)例化結(jié)果，元模型是對(duì)模型的抽象分類。

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

圖2 模型及元素組織結(jié)構(gòu)

使用元模型對(duì)模型進(jìn)行描述實(shí)際上就是使用元模型中的元元素對(duì)模型中的元素進(jìn)行描述，元素是元元素的實(shí)例化結(jié)果，元元素是對(duì)元素的抽象分類，既是用元元素建模的結(jié)果得到元素。元元素與元元元素之間關(guān)系亦然。因此，使用元模型對(duì)模型進(jìn)行描述實(shí)際就是將元模型中的元元素實(shí)例化為模型中的元素。使用元元模型對(duì)元模型進(jìn)行描述實(shí)際上就是將元元模型中的元元元素實(shí)例化為元模型中的元元素。

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

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

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

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

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

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

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

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

2.2類圖元模型形式化

UML標(biāo)準(zhǔn)文檔中給出了類圖元模型包含的所有元元素。在此本文只討論平時(shí)UML建模中設(shè)計(jì)到的類圖元模型的主要元元素Class、Property、Association、Generalization。

圖5 類圖元模型

（1）Class的形式化

面向?qū)ο蟮能浖_發(fā)中將類描述為一組具有共同特征的對(duì)象的集合，表明集合Class中包含的元素在某一方面具有相同的特征。類具有集合的特性。例如元元素DataType類中的對(duì)象指類包含的屬性值的數(shù)據(jù)類型。

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

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

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

一元謂詞：C

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

（2）Attribute的形式化

UML標(biāo)準(zhǔn)文檔中將屬性的語義描述為“通過ownedAttribute與 Class相關(guān)聯(lián)的 property叫做 Attri?bute，Attribute是一個(gè)結(jié)構(gòu)特征。Attribute將類的實(shí)例與Attribute類型相關(guān)聯(lián)”。

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

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

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

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

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

對(duì)應(yīng)的描述邏輯ALCUQI的形式化表示為：

（3）Association的形式化

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

圖7 association連接class

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

Class1、Class2看作兩個(gè)集合，Association是兩集合元素構(gòu)成的笛卡爾集。

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

對(duì)應(yīng)的描述邏輯ALCUQI的形式化表示為：

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

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

②帶角色關(guān)聯(lián)的重?cái)?shù)約束

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

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

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

使用一階邏輯表示是上述語義：對(duì)應(yīng)的描述邏輯ALCUQI的形式化表示為：

（4）Aggregation的形式化

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

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

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

圖10 聚合關(guān)聯(lián)

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

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

對(duì)應(yīng)的描述邏輯ALCUQI的形式化表示為：

（5）Composition的形式化

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

圖11 組合關(guān)聯(lián)

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

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

對(duì)應(yīng)的描述邏輯ALCUQI的形式化表示為：

（6）Generalization的形式化

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

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

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

對(duì)應(yīng)的描述邏輯ALCUQI描述形式為：

2.3類圖元模型的實(shí)例舉例

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

圖12 教師出題

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

3 正確性證明

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

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

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

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

4 結(jié)語

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