李晶晶，江 濤，郭雨婷，李 迪，王米利

(云南民族大學(xué)數(shù)學(xué)與計(jì)算機(jī)科學(xué)學(xué)院昆明650500)

本文在現(xiàn)有的描述邏輯［1-4］知識(shí)表示方法和 UML類圖模型形式化表示方法［5-8］的基礎(chǔ)上，結(jié)合國內(nèi)外UML類圖元模型的相關(guān)成果［9-13］，提出一種UML類圖元模型基于描述邏輯的表示及驗(yàn)證的方法.該方法在UML類圖元模型構(gòu)建的約束規(guī)則集的基礎(chǔ)上，可以有效地實(shí)現(xiàn)UML類圖元模型與其構(gòu)建模型間的一致性驗(yàn)證問題.但是必須說明的是，正如文獻(xiàn)［9-11］中所研究的，本文只是截取了UML類圖元模型的一個(gè)子集進(jìn)行表示和驗(yàn)證.

1 描述邏輯SHOIN(D)

1)在描述邏輯SHOIN(D)語言中，概念和屬性的語法規(guī)則如下［3-4］:

2)語義規(guī)則如下［3-4］:

其中，A表示原子概念，C表示復(fù)合概念，R和S表示抽象角色，T表示具體角色，D表示抽象數(shù)據(jù)類型，d表示具體數(shù)據(jù)類型;┬表示頂層概念，是其他所有概念的父概念;⊥表示底層概念，是矛盾的概念，是所有其他概念的子概念;?表示否定，∩表示合取(conjunction)，∪表示析取(disjunction)，?表示存在量詞(existential quantification)，?表示值限定(value restriction)［3］.

2 約束規(guī)則集的構(gòu)建

2.1 UML類圖元模型的提取

由于UML類圖元模型的龐大性和復(fù)雜性，正如文獻(xiàn)［9-11］中所研究的，本文只截取UML類圖元模型的一個(gè)子集進(jìn)行約束規(guī)則集的構(gòu)建.即對(duì)于UML類圖元模型，我們忽略一些構(gòu)造子.但是，這些處理不會(huì)對(duì)UML類圖元模型的語義一致性產(chǎn)生影響.如圖1是本文截取的UML類圖元模型的一個(gè)子集，該UML類圖元模型包含 Classifier、Class、property、Operation、Parameter以及類圖元模型里面的各種關(guān)系.

2.2 約束規(guī)則集的構(gòu)建

在文獻(xiàn)［2，5-8］中都已經(jīng)給出UML類圖中基本構(gòu)造子在描述邏輯SHOIN(D)中的表示.在此，本文直接給出UML類圖元模型中的泛化關(guān)系和組合關(guān)系基于描述邏輯SHOIN(D)的表示.

2.2.1 泛化關(guān)系的約束規(guī)則

本文只給出 Classifier與 Class、Interface、Signal、Datatype以及Association之間的泛化關(guān)系，Relationship與Association和DirectedRelationship之間的泛化關(guān)系，以及DirectedRelationship與Generalization、InterfaceRealization、Dependency之間的泛化關(guān)系可以類似給出.

1)父類泛化為多個(gè)子類.即，父類Classifier可以泛化為子類 Class、Interface、Signal、Datatype 以及Association:

Class?Classifier，DataType?Classifier，

Interface?Classifier，Association?Classifier，

Signal?Classifier.

2)子類之間的不相交泛化.即，子類Class、Interface、Signal、Datatype 以及 Association 之間互不相交:

Class?? DataType∩? Interface∩?

Association∩? Signal.

DataType?? Class∩? Interface∩?Association∩? Signal.

Interface?? Class∩? DataType∩?

Association∩? Signal.

Association?? Class∩? DataType∩?

Interface∩? Signal.

Signal?? Class∩? DataType∩?

Interface∩? Association.

3)子類之間的完全覆蓋泛化.即，子類Class、Interface、Signal、Datatype 以及 Association 將父類Classifier完全覆蓋:

Classifier≡Class∪DataType∪Interface∪

Association∪Signal.

2.2.2 組合關(guān)系的約束規(guī)則

由圖1的類圖元模型，我們觀察到Class、Interface、Signal、Datatype 以及 Association 都有 Property，且它們與Property之間都是組合關(guān)系.在此我們規(guī)定，對(duì)于一個(gè)具體的Property(P)，當(dāng)Property(P)與Class形成組合關(guān)系時(shí)，Property(P)與Interface、Signal、Datatype以及 Association不形成組合關(guān)系.同理，其他也適用.

Property、Operation與Class之間組合關(guān)系.即，一個(gè)Class可以沒有Property和Operation，也可以有多個(gè)Property和Operation.同樣也適合于Interface、Signal、Datatype以及 Association 中:

Class? (?ownedAttribute.Property)∩ (≥0ownedAttribute.Property)，

Property?(?class.Class)∩(≥0class.Class)∩(≤1class.Class)Class?(?ownedO peration.Operation)∩(≥0ownedOperation.Operation)，

Operation? (?class.Class)∩ (=1class.Class).

2.2.3 類的屬性的約束規(guī)則

1)屬性的重?cái)?shù)約束規(guī)則，如下［7］:

C?(≥min a)∩(≤max a).

其中，類C用原子概念C表示，類的屬性a用原子關(guān)系a表示.注意:屬性上，若多重性沒有給出，缺省值是 0…*［10］.

2)屬性的枚舉值約束規(guī)則.枚舉值表示枚舉元類屬性的列舉值.我們用3條規(guī)則來表達(dá)枚舉元類包含的信息，分別是:枚舉值的可區(qū)分性、枚舉值的類型和枚舉元類的完全性.由于用推理機(jī)Racer對(duì)UML類圖元模型進(jìn)行一致性檢測(cè)過程中，枚舉值的類型和枚舉元類的完全性的影響很小，因此本文只對(duì)枚舉值的可區(qū)分性進(jìn)行描述.

枚舉值的可區(qū)分性規(guī)則用SHOIN(D)表示如下:

其中，原子概念A(yù)1和A2分別對(duì)應(yīng)于枚舉值a和b.

由圖1的類圖元模型，枚舉元類ParameterDirectionKind定義了 4個(gè)枚舉值 in，out，inout和 return.對(duì)ParameterDirectionKind的可區(qū)分性用SHOIN(D)描述如下.

in?? out，in?? inout，in?? return，…，

return?? inout.

in?? out∪? inout∪? return.

out?? in∪? inout∪? return.

inout?? in∪? out∪? return.

return?? in∪? out∪? inout.

2.2.4 關(guān)聯(lián)關(guān)系的約束規(guī)則

1)關(guān)聯(lián)關(guān)系的類型約束規(guī)則.對(duì)由C1到C2之間含有類型A的二元關(guān)聯(lián)，約束規(guī)則如下(如圖2所示):A?C1∩C2.即，對(duì)于從A導(dǎo)出的二元關(guān)系A(chǔ)，若第1個(gè)參數(shù)是以C1為類型的元素，則第2個(gè)參數(shù)必須以C2為類型.

2)關(guān)聯(lián)關(guān)系的多重性約束規(guī)則.對(duì)由C1到C1且?guī)в卸嘀匦訫的二元關(guān)聯(lián)A，根據(jù)M的不同情況，給出以下形式的規(guī)則(如圖2所示):

C1?(≥min A.C2)∩(≤max A.C2);C2?(≥min A-.C1)∩(≤max A-.C1).

注意:關(guān)聯(lián)端點(diǎn)上沒有給出多重性，意味著多重性是 1［10］.

3)帶角色關(guān)聯(lián)的多重性約束規(guī)則.對(duì)由C1到C2的二元關(guān)聯(lián)A，令R1是A在C1端的端點(diǎn)名，R2是A在C2端的端點(diǎn)名，M1是R1上的重?cái)?shù)，M2是R2上的重?cái)?shù)(其中 M1、M2均有 min、max)，則有如下規(guī)則(如圖3所示):

A?R1∩R2∩?R1.C1∩?R2.C2，

C1?(≥min R2.C2)∩(≤max R2.C2)，

C2?(≥min R1.C1)∩(≤max R1.C1).

其中，在關(guān)聯(lián)關(guān)系A(chǔ)中，定義域概念C1實(shí)例的重?cái)?shù)大于最小值min，小于最大值max;值域概念C2實(shí)例的重?cái)?shù)大于最小值min，小于最大值max.

由圖1的類圖元模型，Association與Property之間的關(guān)聯(lián)關(guān)系是一種帶角色和多重性的關(guān)聯(lián)關(guān)系，具體表示如下:

Association?≥2memberEnd.Property，

Property?(≥0association.Association)∪(≤1association.Association).

即關(guān)聯(lián)關(guān)系可以有關(guān)聯(lián)角色和多重性，且當(dāng)關(guān)聯(lián)角色確定以后，關(guān)聯(lián)關(guān)系兩端的類唯一確定.

其他關(guān)聯(lián)關(guān)系之間的規(guī)則同上.

3 一致性驗(yàn)證

3.1 相關(guān)定義

在文獻(xiàn)［13］的基礎(chǔ)上給出以下定義:

定義1:類圖元模型的邏輯一致性.如果一個(gè)類圖元模型的約束規(guī)則集Lx是邏輯一致的，形式化地說，類圖元模型的約束規(guī)則集Lx中的每個(gè)關(guān)系式在推理機(jī)Racer中都不存在矛盾，則我們稱類圖元模型是邏輯一致的;反之，如果一個(gè)類圖元模型的約束規(guī)則集Lx是邏輯不一致的，形式化地說，類圖元模型的約束規(guī)則集Lx中的關(guān)系式之間在推理機(jī)Racer中存在矛盾，則我們稱類圖元模型是邏輯不一致的.

由于手工推理的復(fù)雜性，在此，我們借助推理機(jī)Racer來對(duì)UML類圖元模型進(jìn)行一致性的驗(yàn)證.將UML類圖元模型的約束規(guī)則集放入Racer里面，經(jīng)驗(yàn)證UML類圖元模型是邏輯一致的.

定義2:類圖模型—元模型間的邏輯一致性.如果一個(gè)類圖模型滿足類圖元模型，形式化地說，類圖模型對(duì)應(yīng)的結(jié)構(gòu)語義集L1在推理機(jī)Racer中滿足類圖元模型的約束規(guī)則集Lx，則我們稱類圖模型對(duì)應(yīng)于類圖元模型是邏輯一致的;反之，如果一個(gè)類圖模型不滿足類圖元模型，形式化地說，類圖模型對(duì)應(yīng)的結(jié)構(gòu)語義集L1在推理機(jī)Racer中存在不滿足類圖元模型的約束規(guī)則集Lx，則我們稱類圖模型對(duì)應(yīng)于類圖元模型是邏輯不一致的.

其中，L1表示類圖模型基于描述邏輯SHOIN(D)的結(jié)構(gòu)語義集，Lx表示類圖元模型基于描述邏輯SHOIN(D)的約束規(guī)則集.

3.2 模型研究

在此，我們借助推理機(jī)Racer對(duì)UML類圖模型進(jìn)行一致性的驗(yàn)證.將UML類圖元模型的約束規(guī)則集和UML類圖模型的結(jié)構(gòu)語義集放入Racer里面.經(jīng)驗(yàn)證，UML類圖模型里面存在以下矛盾:

1)Student與Doctor和Graduate之間的泛化關(guān)系違背了子類的完全覆蓋泛化規(guī)則.

眾所周知，University里面的Student一定包含UniversityStudent.即，一定存在

Class(Universitystudent)?Class(Student).

而圖4中的UML類圖模型里面的Student只包含Doctor和Graduate.即，只存在

Class(Doctor)?Class(Student)，

Class(Graduate)?Class(Student).

2)Mary與Doctor和Graduate之間的泛化關(guān)系違背了子類的不相交泛化規(guī)則.

作為一名具體的學(xué)生類Mary，她即是Doctor又是Graduate.即，下列結(jié)構(gòu)語義同時(shí)存在

Class(Mary)?Class(Doctor)，

Class(Mary)?Class(Graduate).

這在類圖里面是不允許的，且與現(xiàn)實(shí)情況不相符.

3)Student與Course以及Course與Instructor之間的關(guān)聯(lián)關(guān)系均違背了關(guān)聯(lián)關(guān)系的類型約束規(guī)則.

Student與Course之間是Attends的關(guān)系，Course與Instructor之間是 Teacher的關(guān)系.而圖4中的UML類圖模型得到的結(jié)構(gòu)語義規(guī)則與之正好相反.

Association(Teacher)?Class(Student)∩Class(Course)，

Association(Attends)?Class(Course)∩Class(Instructor).

由上述驗(yàn)證結(jié)果可知，該UML類圖模型對(duì)應(yīng)于UML類圖元模型是邏輯不一致的.

4 結(jié)語

本文針對(duì)UML類圖元模型的非形式化表示方法，在深入分析UML類圖模型形式化表示及提取UML類圖元模型的一個(gè)子集的基礎(chǔ)上，構(gòu)建了UML類圖元模型基于描述邏輯SHOIN(D)的約束規(guī)則集，并借助推理工具Racer驗(yàn)證了UML類圖元模型與其構(gòu)建模型之間的一致性.下一步的工作包括不斷完善UML類圖元模型的約束規(guī)則集、開發(fā)一種軟件來實(shí)現(xiàn)UML類圖元模型的自動(dòng)推理引擎以及對(duì)UML類圖模型的自動(dòng)形式化描述與一致性驗(yàn)證功能.

［1］Object Management Group.OMG final adopted specification［EB/OL］.［2006-8-23］http://www.omg.org/bpmn/Documents/OMG_Final_Adopted_BPMN_1-0_Spec_06-02-01.Pdf.

［2］吳建，鄭潮，汪杰.UML基礎(chǔ)與Rose建模案例［M］.北京:人民郵電出版社，2004.

［3］BAADER F，NUTT W.Basic description logic［M］.Cambridge，UK:Cambridge University Press，2003.

［4］ROSSI F，BEEK P，WALSH T.Handbook of Constraint Programming［M］.Amsterdam:Elsevier，2006.

［5］郝斐，董慶超，曾廣軍.一種基于描述邏輯的UML模型驗(yàn)證方法［J］.計(jì)算機(jī)與數(shù)字工程，2011(11):58-62.

［6］齊玉東，楊斌，李瑛，等.基于描述邏輯的Onto UML模型的形式化表示［J］.計(jì)算機(jī)工程與科學(xué)，2012(7):89-92.

［7］董慶超，王智學(xué)，張愛輝，等.基于UML類圖模型的一致性檢查方法［J］.計(jì)算機(jī)技術(shù)與發(fā)展，2008(10):85-88.

［8］陳振慶.基于SHOIN(D)的UML類圖形式化方法［J］.計(jì)算機(jī)工程與科學(xué)，2009(19):43-45.

［9］單黎君，朱鴻.UML的形式化描述語義［J］.計(jì)算機(jī)工程與科學(xué)，2010(3):96-103.

［10］單黎君.圖形的一致性檢查［D］.長(zhǎng)沙:國防科學(xué)技術(shù)大學(xué)，2008.

［11］BERARDI D，CALVANESE D，GIACOMO G.Reasoning on UML class diagrams［J］.Artificial Intelligence，2005，168(3):70-118.

［12］沈國華，張偉，黃志球，等.基于描述邏輯的特征語義建模及驗(yàn)證［J］.計(jì)算機(jī)研究與發(fā)展，2013(7):1501-1512.

［13］JIANG Tao，WANG Xin.Research on meta-models consistency verification based on formalization of domainspecific metamodeling language［J］.上海交通大學(xué)學(xué)報(bào):英文版，2012，17(2):171-177.