UML類圖元模型基于描述邏輯的表示及驗證

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

(云南民族大學數學與計算機科學學院昆明650500)

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

1 描述邏輯SHOIN(D)

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

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

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

2 約束規則集的構建

2.1 UML類圖元模型的提取

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

2.2 約束規則集的構建

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

2.2.1 泛化關系的約束規則

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

1)父類泛化為多個子類.即，父類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 組合關系的約束規則

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

Property、Operation與Class之間組合關系.即，一個Class可以沒有Property和Operation，也可以有多個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 類的屬性的約束規則

1)屬性的重數約束規則，如下［7］:

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

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

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

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

其中，原子概念A1和A2分別對應于枚舉值a和b.

由圖1的類圖元模型，枚舉元類ParameterDirectionKind定義了 4個枚舉值 in，out，inout和 return.對ParameterDirectionKind的可區分性用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 關聯關系的約束規則

1)關聯關系的類型約束規則.對由C1到C2之間含有類型A的二元關聯，約束規則如下(如圖2所示):A?C1∩C2.即，對于從A導出的二元關系A，若第1個參數是以C1為類型的元素，則第2個參數必須以C2為類型.

2)關聯關系的多重性約束規則.對由C1到C1且帶有多重性M的二元關聯A，根據M的不同情況，給出以下形式的規則(如圖2所示):

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

注意:關聯端點上沒有給出多重性，意味著多重性是 1［10］.

3)帶角色關聯的多重性約束規則.對由C1到C2的二元關聯A，令R1是A在C1端的端點名，R2是A在C2端的端點名，M1是R1上的重數，M2是R2上的重數(其中 M1、M2均有 min、max)，則有如下規則(如圖3所示):

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

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

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

其中，在關聯關系A中，定義域概念C1實例的重數大于最小值min，小于最大值max;值域概念C2實例的重數大于最小值min，小于最大值max.

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

Association?≥2memberEnd.Property，

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

即關聯關系可以有關聯角色和多重性，且當關聯角色確定以后，關聯關系兩端的類唯一確定.

其他關聯關系之間的規則同上.

3 一致性驗證

3.1 相關定義

在文獻［13］的基礎上給出以下定義:

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

由于手工推理的復雜性，在此，我們借助推理機Racer來對UML類圖元模型進行一致性的驗證.將UML類圖元模型的約束規則集放入Racer里面，經驗證UML類圖元模型是邏輯一致的.

定義2:類圖模型—元模型間的邏輯一致性.如果一個類圖模型滿足類圖元模型，形式化地說，類圖模型對應的結構語義集L1在推理機Racer中滿足類圖元模型的約束規則集Lx，則我們稱類圖模型對應于類圖元模型是邏輯一致的;反之，如果一個類圖模型不滿足類圖元模型，形式化地說，類圖模型對應的結構語義集L1在推理機Racer中存在不滿足類圖元模型的約束規則集Lx，則我們稱類圖模型對應于類圖元模型是邏輯不一致的.

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

3.2 模型研究

在此，我們借助推理機Racer對UML類圖模型進行一致性的驗證.將UML類圖元模型的約束規則集和UML類圖模型的結構語義集放入Racer里面.經驗證，UML類圖模型里面存在以下矛盾:

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

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

Class(Universitystudent)?Class(Student).

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

Class(Doctor)?Class(Student)，

Class(Graduate)?Class(Student).

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

作為一名具體的學生類Mary，她即是Doctor又是Graduate.即，下列結構語義同時存在

Class(Mary)?Class(Doctor)，

Class(Mary)?Class(Graduate).

這在類圖里面是不允許的，且與現實情況不相符.

3)Student與Course以及Course與Instructor之間的關聯關系均違背了關聯關系的類型約束規則.

Student與Course之間是Attends的關系，Course與Instructor之間是 Teacher的關系.而圖4中的UML類圖模型得到的結構語義規則與之正好相反.

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

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

由上述驗證結果可知，該UML類圖模型對應于UML類圖元模型是邏輯不一致的.

4 結語

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

［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基礎與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模型驗證方法［J］.計算機與數字工程，2011(11):58-62.

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

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

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

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

［10］單黎君.圖形的一致性檢查［D］.長沙:國防科學技術大學，2008.

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

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

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