基于描述逻辑ALCUQI的UML类图元模型形式化方法

杨小钢

（重庆邮电大学软件工程学院，重庆 400065）

0 引言

UML类图是一种图形化的建模语言，虽然其表示直观，但它却是一种半形式化的语言，缺乏精确的形式化语义表示，难易保证建立模型语义的一致性。而且对于模型语义一致性的检测往往是靠人工检测，实现模型一致性的自动检测是一件十分有价值的事。描述逻辑能对领域知识进行形式化的表示，同时描述逻辑还提供有相应的推理服务。本文采用基于描述逻辑的方法，研究类图的元模型中元元素与描述逻辑间的对应关系，实现类图元模型的形式化转化。

1 描述逻辑ALCUQI

描述逻辑是一种对领域知识表示的形式化语言，适合表示关于概念与概念层次结构的知识[1]。描述逻辑语言的名称与描述逻辑中包含的构造算子有关。AL是描述逻辑中最为基本的描述逻辑语言，任何其他的描述语言都是在AL的基础之上扩展得到的。在AL语言当中，否定是只能被用于原子概念中，而且在角色存在变量范围的情况下是只允许使用全局变量的[2]。

描述逻辑ALCUQI的语法和语义：

描述逻辑ALCUQI是在AL的基础扩展到角色逆算子和有限制的数量约束算子得来的。

定义令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类图元模型形式化背景及思路

本节首先介绍类图元模型的形式化背景，介绍元对象机制MOF，分析模型与元模型间的对应关系，然后介绍本文进行类图元模型形式化的思路。

（1）类图元模型的形式化背景

模型是模型驱动开发过程中的核心，是对客观世界中事物的抽象，也是事物传递的信息的载体。元模型是描述模型的模型，可以将元模型看作是描述模型的一种语言。元对象机制MOF是国际对象组织OMG提出的一种对元模型进行描述的规范的公共抽象定义语言。MOF将元模型的体系结构分为4层：M0信息层、M1模型层、M2元模型、M3元元模型层，四层之间的关系[3]。如图1所示。

图1 MOF体系结构

从模型层面来看，人们使用模型对客观世界中存在的事物进行描述，使用元模型对模型进行描述，使用元元模型对元模型进行描述。多个模型可以由一个元模型来描述，多个元模型可以由一个元元模型来描述。例如模型可以看作是元模型的实例化结果，元模型是对模型的抽象分类。

从元素层面来看，模型是由一个或者多个元素组成，元模型是由一个或者多个元元素组成，元元模型是由一个或者多个元元元素组成。如图2所示。

图2 模型及元素组织结构

使用元模型对模型进行描述实际上就是使用元模型中的元元素对模型中的元素进行描述，元素是元元素的实例化结果，元元素是对元素的抽象分类，既是用元元素建模的结果得到元素。元元素与元元元素之间关系亦然。因此，使用元模型对模型进行描述实际就是将元模型中的元元素实例化为模型中的元素。使用元元模型对元模型进行描述实际上就是将元元模型中的元元元素实例化为元模型中的元元素。

（2）类图元模型的形式化思路

从图3中可以看出多维数据模型是在MOF的M1模型层，多维数据元模型在MOF的M2元模型层。多维数据模型和多维数据元模型的关系与模型和元模型的关系相同，多维数据元模型用来描述多维数据模型，多维数据模型是多维数据元模型的实例化结果。多维数据元模型是多维数据模型的元模型，多维数据元模型是将多维所具有的特点如事实、维、级别、层次、度量等元素按照类图的关联约束进行组织的。多维数据模型的知识表示与类图不同，多维数据模型的组成元素是由复杂的对象构成，若直接对多维数据模型中的组成元素表示为描述逻辑中的概念或者角色，就会造成语义的缺失[4]。

图3 关系数据模型与多维数据模型之间的关联

为了解决使用描述逻辑直接表示多维数据模型存在的问题，本文使用多维数据元模型表示出多维数据模型，使用类图元模型表示多维数据元模型。从而间接地表示出多维数据模型。如图4所示。

图4 类图元模型形式化思路

对多维数据元模型形式化，就是根据语义对多维数据元模型中的元素进行形式化。多维数据元模型继承关系数据元模型，所以多维数据元模型中的元素是关系数据元模型中元素集合的子集。所以首先需要对关系数据模型中的元素形式化。关系数据模型中的元素是由关系数据元模型中的元元素描述，所以对关系数据模型中的元素形式化首先需要对关系数据元模型中的元元素进行形式化。

CWM中的元模型都是使用类图进行组织的[4]，所以多维数据元模型是由类图元模型进行描述。类图元模型此时属于MOF中的M3元元模型层，类图元模型中的元元素此时就是元元元素。即多维数据元模型中的元元素由类图元模型中的元元素进行描述。

综上所述，对多维数据模型的形式化转化为根据语义对组成类图元模型的元元素进行形式化。

2.2类图元模型形式化

UML标准文档中给出了类图元模型包含的所有元元素。在此本文只讨论平时UML建模中设计到的类图元模型的主要元元素Class、Property、Association、Generalization。

图5 类图元模型

（1）Class的形式化

面向对象的软件开发中将类描述为一组具有共同特征的对象的集合，表明集合Class中包含的元素在某一方面具有相同的特征。类具有集合的特性。例如元元素DataType类中的对象指类包含的属性值的数据类型。

用集合表示元元素Class的语义：

ClassI={o|o是类图中的元元素类}

使用一阶逻辑表示Class的语义：

一元谓词：C

等同于描述逻辑ALCUQI的概念C。

（2）Attribute的形式化

UML标准文档中将属性的语义描述为“通过ownedAttribute与 Class相关联的 property叫做 Attri⁃bute，Attribute是一个结构特征。Attribute将类的实例与Attribute类型相关联”。

图5中元元素Class和元元素property的组合语义表明Attribute是Class的组成元素，并且Attribute所代表的属性值还具有特定的数据类型。通过对类图元模型中元元素Class、Attribute和DataType三者间关联语义的分析如图6。

图6 Class、Attribute和DataType三者间关联

因此，将 Attribute作为一个集合，将 Class和DataType看作两个集合，Attribute作为 Class和DataType两个集合元素所构成的笛卡尔集。

用集合表示元元素Attribute的语义：

使用一阶逻辑表示Attribute与Class、DataType之间关联的语义为：

对应的描述逻辑ALCUQI的形式化表示为：

（3）Association的形式化

图5中元元素property和association的组合关联中property的角色ownedend表明property是被associ⁃ation拥有的端，除此外，property和association的二元关联中property的角色是成员端 memberend，表示property是association的组成成员，由于property的基数约束是2…*，即一个association拥有两个或者prop⁃erty。另外，图中可看到property与class存在组合关系，property在该关联中是ownedAttribute角色，表示property是class的成员，根据重数可知一个property属于一个class。所以，一个association连接两个或多个class。根据上述整理得到类图中association连接class的语义如图7。

图7 association连接class

①用集合表示元元素Association的语义：

Class1、Class2看作两个集合，Association是两集合元素构成的笛卡尔集。

使用一阶逻辑表示Association与Class1、Class2之间关联的语义为：

对应的描述逻辑ALCUQI的形式化表示为：

值得注意的是一般的二元关联Association除了包含关联名外，还拥有关联两端的关联角色，并且角色是具有多重性（用[i,j]表示），表示通过关联由多少个对象参与该关联。

图8 带关联名和角色的二元关联

②带角色关联的重数约束

图8中通过关联Association（关联名为Associa⁃tion）连接的Class1对象的角色是Class1且重数约束是0…1。Class1、Class2看作两个集合，Association是两集合元素构成的笛卡尔集（xi表示Class1的元素，yi表示Class2的元素，（xi,yi）代表集合class1，（yi,xi）代表集合class2，class1∪class2=Association）。

使用一阶逻辑表示是上述语义：

图8中通过关联Association连接的Class2对象的角色是class2且重数约束是0…1。Class1、Class2看作两个集合，Association是两集合元素构成的笛卡尔集（xi表示Class1的元素，yi表示Class2的元素，（xi,yi）代表集合Class1，（yi,xi）代表集合class2，class1∪class2=Association）。

使用一阶逻辑表示是上述语义：对应的描述逻辑ALCUQI的形式化表示为：

（4）Aggregation的形式化

在UML建模中将关联细分为一般二元关联、聚合关联、组合关联。从图5类图元模型中可以看出元元素Association通过和元元素Type的关联来指定关联的类型。结合2.2.3小节中一般二元关联的描述归纳得到聚合的关联关系如图9。

图9 关联与类型

二元关联中有一种特殊形式是聚集，也称聚合，表示整体与部分之间的关系。整体一端用一个实心的菱形箭头表示。表示各部分的生命周期独立于整体，而且一个部分可同时属于多个整体[8]。如图10元元素Class1由Class2聚合而成，Class1消失后Class2也可独立存在（此处聚合关联的关联名为Aggregation）。

图10 聚合关联

用集合表示元元素Aggregation的语义：

使用一阶逻辑表示Aggregation与Class1、Class2之间关联的语义为：

对应的描述逻辑ALCUQI的形式化表示为：

（5）Composition的形式化

组合是聚合的强关联形式，比聚合多了2个约束，第一个约束是部件实例只能同时包含在至多1个组合实例中，这就要求组合管理端重数的上边界不能大于1；第二个约束是强调部件具有与组合相同的生命周期[4]。组合如图11，元元素Class1由Class2组合而成，一旦Class1消失Class2随之消失（此处聚合关联的关联名为 Composition）。

图11 组合关联

用集合表示元元素Composition的语义：

使用一阶逻辑表示Composition与Class1、Class2之间关联的语义为：

对应的描述逻辑ALCUQI的形式化表示为：

（6）Generalization的形式化

图5类图元模型中元元素Class自身存在自关联，自关联中有superClass和class两端，superClass代表超类即父类，class端代表子类。用集合论术语来说，超类对象是一个集合，其子类对象集合是它的一个子集合[8]。用泛化关系可组合一个有层次的概念结构。如图5中Class继承Classifier。

用集合表示元元素Generalization的语义：

使用一阶逻辑表示Class继承Classifier的语义为：

对应的描述逻辑ALCUQI描述形式为：

2.3类图元模型的实例举例

图12是类图元模型的实例举例，描述的是题库系统中教师出题的场景，一个教师属于一个学院，教师和学院之间存在聚合关联，教师作为出题人出考试题，一个教师可以出多个试题，教师和试题间存在出题的二元关联，试题和答案选项之间存在组合管理，一个试题包含多个答案选项，教师继承系统中用户的一部分功能。

图12 教师出题

根据2.2节中类图元模型的形式化方法，图12教师出题实例在描述逻辑ALCUQI的描述逻辑表示如下：

3 正确性证明

通过上述分析可知，类图元模型的元元素与描述逻辑ALCUQI具有对应关系，类图元模型的元元素可以转化为描述逻辑ALCUQI的知识库。描述逻辑AL⁃CUQI知识库KB包含Tbox和Abox。Tbox引入应用领域中的术语表（terminology）；Abox包含对个体的实例断言（instance assertion）和关系断言（role assertion）。此外描述逻辑还提供了推理服务[1]。描述逻辑ALCUQI的解释I=(△I,.I)，其中，△I是解释论域；.I是解释函数。如果解释I=(△I,.I)满足知识库KB中的所有断言，则I是KB的一个模型。如果知识库KB存在一个模型，则KB 是可满足的。对于知识库中的一个概念C，如果存在一个KB的一个模型I则称概念C是可满足的[9]。

类图元模型元元素与描述逻辑ALCUQI知识库间的转化可以通过设计一个函数f来实现。转化函数f的正确性证明如下：

假设M是类图元模型的一个模型，f（M）是转化后的描述逻辑ALCUQI的知识库。由于类图元模型M的元元素的语义可以转化为一阶谓词逻辑FOL，表示元元素能转化为一阶谓词逻辑公式集合，因此转化过程的正确性证明只要对于任意解释I，I满足M转化得到的一阶逻辑公式集合FOL（M），当且仅当I满足转化得到的ALCUQI知识库f（M）。

接下来对类Class的数据类型为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进行知识可满足性的推理，实现类图元模型实例化后模型的一致性检测。本文提出的基于描述逻辑ALCUQI的类图元模型形式化方法为UML模型形式化和一致性自动检测的研究提供了参考价值。