UML类图的形式规约与精化研究

王博文 盛 枫 窦 亮 杨宗源

(华东师范大学信息科学技术学院 上海 200241)

UML类图的形式规约与精化研究

王博文 盛 枫 窦 亮 杨宗源

(华东师范大学信息科学技术学院 上海 200241)

UML由于其广泛的应用和直观的图形化符号，成为了模型驱动工程的重要组成部分。但UML本身缺乏精确的形式语义定义，缺少对其模型精化关系的形式化规范定义，对UML模型进行形式验证变得尤为困难。UML类图作为描述系统结构的静态模型，不具备完整的形式语义。从UML类图的机械语义中抽取出形式规约，将UML类图中的结构和形式规约转换成定理证明器Coq中的机械语义定义。此外，还提出了类图的结构精化操作，将模型间的精化关系在Coq中进行形式化定义，并且对精化操作的原子操作进行机械验证，保证其精化前后系统的结构和语义保持一致。将UML和形式化方法相结合，为可验证的软件设计精化框架提供了理论依据。

UML类图 模型精化 Coq 机械语意

0 引 言

统一建模语言UML是一种通用的图形化建模语言，具备直观易懂特性，并且具有较好的可视化工具提供支持如Rational Rose、 Argo UML等，在模型驱动工程中得到了广泛的应用，成为面向对象分析和设计的工业标准。UML提供不同类型的图，从不同方面和不同视角对系统进行建模。然而，当前的UML2.0使用半形式化的图、约束和非形式化的自然语言文本进行描述，缺乏精确的语义定义，会导致以下问题：(1)对模型理解的不一致性，即不同的人员对同一模型会有不同的理解；(2)难以实现迭代精化的开发过程；(3)难以对模型进行分析以保证其正确性。

在之前的工作中[4]，我们使用定理证明器Coq[3]对UML序列图和状态图的机械语义与精化操作进行形式化描述和机械验证，并使用Kermeta[14]实现了序列图和状态图的形式语义到Coq定义的自动转换。然而，由于序列图和状态图是UML动态图，具有完整的指称语义或操作语义，可在Coq中描述并实现机械验证。UML类图作为描述系统结构的静态模型，不具备完整的形式语义，因此本文首先从UML类图的形式语义中抽取出形式规约，即形式规约是UML类图形式语义的具体体现。然后使用Coq对UML类图的形式规约和结构精化的原子操作进行形式化描述与定义。基于上述的形式描述，将UML类图的重要属性与精化关系转换为数学定理，在Coq中进行形式化定义与验证。本文将半形式化的UML类图与形式化方法相结合，弥补了半形式化UML的不足，通过对类图及其精化操作的形式化描述与验证，保证UML模型及其精化的一致性和正确性，为可验证软件设计模型精化框架提供了理论基础。

1 定理证明器Coq

Coq是当前被广泛用于机械语义研究的交互式定理证明器，其内置语言(Gallina)基于归纳构造演算，且提供交互式的证明环境。归纳构造演算是一种形式系统，结合了构造逻辑和依赖类型的最新进展。Coq中的归纳类型扩展了传统程序设计语言中有关类型定义的概念，融合递归类型和依赖积，具有更强的表达能力。与其他证明工具相比，Coq尤为适合对形式语法和语义进行精确的表示。如Isabelle/HOL也可用于机械语义验证，但由于Isabelle/HOL[13]缺乏依赖类型，因此对一些正确性属性的证明代码量相对较多。Coq中常用的类型包括归纳类型和归纳谓词。归纳类型适合对数据类型进行建模，它可以表示无限集合，且每个元素都是在有限步骤内构造的。归纳谓词可以对各种属性进行公式化，并可表示各种归纳数据类型之间的关系，适合描述系统之间的重要属性。

Coq使用归纳类型来定义类型。例如，自然数的归纳类型可定义为：

Inductive nat ：Set :=

| O : nat | S : nat -> nat.

其中nat是归纳定义类型，属于Set(类型的全域)中的值。类型nat包括两个构造子，第一个构造子声明O属于自然数，第二个构造子表示任意给定一个自然数n，S n仍然是个自然数，即任何自然数的后继也是自然数。Coq还可以表示归纳定义的谓词，表示数据类型的属性或关系。基于类型nat的定义，可以定义偶数的概念：

Inductive even : nat -> Prop :=

| O_even: even O

| Plus2_even: forall n:nat, even n -> even (S (S n)).

谓词even的类型是nat->Prop，表示关于nat的命题。even n是n是偶数的一个证明。O_even表示 O 是偶数，Plus2_even表示对于任意的自然数n，如果n是偶数，则n+2也是偶数。关键字Definition用来定义新的数据类型，如Definition string_pair : Set := string * string定义了类型(string，string)。

2 类图形式规约

UML的类图是由多个类，类之间的关系以及这些关系的约束组成，是描述系统结构的一种静态模型，是构建UML其他图的基础。类图所包含的内容有：类、关联、关联类和泛化等。本节将介绍UML类图中各个元素的形式规约，并且在定理证明器Coq中形式化描述。

2.1 类

类是描述具有相同特征、约束和语义的一组对象的集合，是构成类图的基础。在语法上，一个类是由类名、属性和操作组成的，其中属性由属性名和属性类型组成，操作由操作名和操作参数组成，每个操作参数具有参数名和参数类型。根据Evans[1]的UML类图语法，本文定义ClassName和Name来表示类名与属性、操作名集合：ClassName表示所有类的名字的集合，Name表示所有属性、操作以及操作参数名的集合。使用ClassDec =(P，O，attrtype, opsigs)来形式定义类，其中P表示属性的集合，O表示操作集合，attrtype函数将类中的属性映射到属性类型，具有Name -> Type类型，opsigs函数将类中的操作映射到相应的操作参数，并且将参数映射到参数类型，具有Name -> (Name -> Type)类型。在Coq中，使用归纳类型定义包括类名(Class)，属性(Property)，操作(Operation)和参数(Parameter_)等基本类型，关键字 Definition定义类型ClassDec：

Inductive Class : Set := class : string -> Class.

Inductive Operation : Set := operation : string -> Operation.

Inductive Property : Set := property : string -> Property.

Inductive Parameter_ : Set :=parameter : string ->

Parameter_.Definition ClassDec : Type :=

list Property * list Operation * (Name -> Type) * (Name -> (Name -> Type)).其中dom(attrtype) = P, dom(opsigs) = O.

对于属性、操作等类型，不同的类可能具有相同的属性名或操作名，而对于类名来说，不同类的类名必须是不同的。因此，UML类图中的类可定义为类名Class到四元组ClassDec的归纳类型：

Inductive UMLClass := class2dec : Class -> ClassDec -> UMLClass.

2.2 关 联

在UML中，关联关系表示类与类之间的关系，关联可分为三类：一般关联、聚合以及组合。聚合是一种特殊的关联关系，表示类间的关系是整体和部分的关系。组合则是更强形式的关联，整体有管理部分特有的职责并且具有一致的生命周期。在大部分情况下，类图中的关联指的是二元关联，因此，本文仅仅考虑二元关联。

在语法上，二元关联用连接两个类的实线表示，由关联名和一对关联端点(association end)组成。每个关联端点具有角色名(role name)、多重性约束(multiplicity constraint)、附加类(attached class)和关联类型(assockind)等元素。扩展集合Name的定义域，使其包括所有可能的关联名和角色名。关联端点由四元组AssociationEnd = (rolename, multiplicity, attachedclass, aggregation)表示。UML类图的多重性约束表示一个类与相关联的类的单个实例可能相关的实例个数，即多重性约束了相关对象的数目。因此，本文使用自然数域(nat)来表示多重性的上界。附加类表示其与该关联端点相连接的类，具有Class类型。aggregation表示关联类型，具有一般关联(none)，聚合(aggregate)和组合(composite)三种类型。在Coq中使用归纳类型Indutive来定义关联类型：

Inductive assockind := none | aggregate | composite.

Definition AssociationEnd : Type := string * nat * Class * assockind.Definition associations:= string * (AssociationEnd * AssociationEnd).

其中nat表示自然数集合。对于关联关系来说，具有以下约束条件：

定义1 对于一组关联关系(n, (e1,e2))，关联名n与角色名e1.rolename、e2.rolename不能相同。

Definition asso_post1 (assoc : set associations):=

forall (n : string) (e1 e2 : AssociationEnd), set_In (n, (e1, e2)) assoc -> (rolename e1) <> (rolename e2) ∧ n <> (rolename e1) ∧ n <> (rolename e2).

其中set_In函数是Coq内置函数，用于判定某个元素是否属于某个集合。

定义2 对于聚类关系，两个关联端点的关联类型分别为aggregate和none；对于组合关系，两个关联端点的关联类型分别为composite和none；对于组合关系，关联端点的关联类型为composite的端点，其多重性约束的值为1。

Definition asso_post2 (assoc : set associations):=

forall (n : string) (e1 e2 : AssociationEnd), set_In (n, (e1, e2)) assoc -> (or (aggregation e1 = composite) (aggregation e1 = aggregate) -> aggregation e2 = none) ∧(aggregation e1 = composite -> multiplicity e1 = 1).

函数or表示Coq内置的逻辑或操作。

定义3 对于所有的关联关系，其关联名必须是唯一的，即如果 (n1,(e1,e2))和(n2,(e3,e4))均属于集合associations，e1 ≠ e3，e2 ≠ e4，e1对应的附加类与e3相同且e2对应的附加类与e4相同，那么n1≠n2。

Definition asso_post3 (assoc : set associations):= forall (n1 n2 : string) (e1 e2 e3 e4 : AssociationEnd) ,

e1 <> e3 ∧ e2 <> e4 ∧ set_In (n1, (e1, e2)) assoc ∧ set_In (n2, (e3, e4)) assoc ∧attechedclass e1 = attechedclass e3 ∧ attechedclass e2 = attechedclass e4 -> n1 <> n2.

如果类图中的关联关系符合上述语法和约束，则认为其符合UML类图的形式规范。使用Coq中的子集类型来表示符合上述约束的数据类型，即将数据类型和该类型上的约束谓词相结合，从而得到满足该谓词的数据类型：

Definition umlassociations :=

{assoc : set associations | asso_post1 assoc ∧ asso_post2 assoc ∧ asso_post3 assoc }.

2.3 关联类

关联类是一个拥有关联关系和类特性的模型元素。一个关联类可以看作是一组拥有类特性的关联关系，或者是一个拥有关联特性的类。它不仅仅用于连接一些分类器(classifier)，还定义了属于关联关系本身的特征，这些特征是只属于关联关系本身而不属于任何关联分类器的。关联类由类和一对关联端点组成，由二元组AssocClassDec = (assoc, (assoEnd1, assoEnd2))表示，其中assoc表示类，是集合umlclass的元素，assoEnd1和assoEnd2是类型AssociationEnd的关联端点：

Definition AssocClassDec: Type := umlclass* (AssociationEnd * AssociationEnd).

对于关联类来说，具有以下约束条件：

定义4 对于任意关联类(umlclass,(e1,e2))，e1.rolename ≠ e2.roolename，并且关联类型的值必须是none。

Definition assocClass_post1 (asscl : UMLAssocClass) := forall (e1 e2 : AssociationEnd),

asslink1 asscl = e1 ∧ asslink2 asscl = e2 -> rolename e1 <> rolename e2 ∧aggregation e1 = none ∧ aggregation e2 = none.

其中函数asslink1和asslink2表示关联类中的一组关联端点，函数rolename表示关联端点中的角色名。

定义5 对于任意关联类(umlclass,(e1,e2))，附加类中的角色名不属于关联类中类的属性名集合。

Definition assocClass_post2 (asscl :set AssocClassDec) :=

forall (u : umlclass) (e1 e2 : AssociationEnd), set_In (u, (e1, e2)) asscl ->set_In (rolename e1) (makeattr_name (class_pro u)) ∧

～ set_In (rolename e2) (makeattr_name (class_pro u)).

其中函数class_pro返回类u中的属性集合，函数makeattr_name将属性集合中的元素类型由Property转换为string类型。

定义6 对于任意关联类(umlclass,(e1,e2))，关联端点中的附加类不是关联类中的类，即e1.attachedclass ≠ umlclass.classname并且e2.attachedclass ≠ umlclass.classname。

Definition assocClass_post3 (asscl : set AssocClassDec) :=

forall (u : umlclass) (e1 e2 : AssociationEnd), set_In (u, (e1, e2)) asscl ->class_eq (attechedclass e1) (class_name u) = false /〗～class_eq (attechedclass e2) (class_name u) = false.

其中函数class_eq判定两个类型为Class的元素是否相等。

UML类图的关联类的形式化表示是满足上述约束的类型为AssocClassDec的数据类型：

Definition UMLAssocClass :=

{ assocClass : AssocClassDec | assocClass_post1 assocClass ∧ assocClass_post2 assocClass ∧ assocClass_post3 assocClass }.

2.4 泛 化

泛化关系是父类与子类之间的关系，子类继承父类的属性和操作，并且添加新的属性和操作，或者修改父类的某些操作[2]，是实现多态的基础。本文使用集合superclasses和subclasses表示泛化关系中的父类和子类。superclasses表示类名Class中的父类的有限集合，subclasseses表示类名Class的每个父类的子类集合的集合。使用二元组(class, subclasees)表示一组泛化关系，其中class表示父类，subclasses表示该父类下的子类集合，列表类型list来定义泛化关系的集合：

Definition UMLGeneralizetion: Type := list (Class * set Class).

Fixpoint subclasses (gen : UMLGeneralizetion) (c : Class): Cl :=

match gen with

| nil => nil

| x :: A => if class_dec (fst x) c then (snd x) else subclasses A c

end.

Fixpoint superclasses (gen : GenDec) : Cl =

match gen with

| nil => nil

| x :: A => (fst x) :: superclasses A

end.

其中fst函数返回多元组中的第一个元素，snd函数是返回多元组中的第二个元素，subclasses函数是对于给定的父类，从泛化关系集合中返回其对应的子类集合; superclasses函数的功能是返回泛化关系集合中的所有父类集合，中缀::表示连接一个元素(fst x)与集合(superclasses A)，将元素置入列表的首位。

对于泛化关系而言，具有以下约束：

定义7 对于任意泛化关系，父类与子类均不具备自反继承性(reflexive inheritance)，即每一个类不可能是该类的父类，也不是该类的子类，父类集合与子类集合不相交。

Definition Gen_post1 (gen : GenDec) :=

forall (cl : Class), set_In cl (superclasses gen) ->

forall (s : Class), set_In s (superclasses gen) -> ～ set_In cl (subclasses gen s).

Definition Gen_post2 (gen : GenDec) :=

forall (cl s : Class), set_In s (superclasses gen) ∧ set_In cl (subclasses gen s) ->

～ set_In cl (superclasses gen).

UML类图中的泛化关系的形式化表示是满足上述约束的类型为GenDec的数据类型：

Definition umlgenalizations := {gen : GenDec | Gen_post1 gen ∧ Gen_post2 gen }.

2.5 类 图

UML类图是包括类、关联类、关联关系和泛化关系等类型的集合，由四元组UMLClassDiagram= (UMLClass, UMLAssociation, UMLAssocClass, UMLGeneralizetion)表示：

Definition UMLClassDiagram := (list UMLClass * UMLAssociation * UMLAssocClass * UMLGeneralizetion).

对于类图而言，具有以下约束：

定义8 类图中的UMLClass集合的类名集合与关联类UMLAssocClass的类名集合不相交。

Definition UMLCD_post1 (umlcd : UMLClassDiagram) : Prop := forall (c : Class), set_In c (makeclass_name (uml_class umlcd)) -> set_In c (assoc_classname (uml_assocclass umlcd)).

其中函数uml_assocclass从类图中取出关联类UMLAssocClass的集合，函数assoc_classname返回关联类UMLAssocClass中的类名集合，函数makeclass_name返回UMLClass集合中的类名集合。

定义9 类图中的关联关系UMLAssociation中的附加类名属于集合UMLClass的类名集合。

Definition UMLCD_post2 (umlcd : UMLClassDiagram) : Prop := forall (c : Class), set_In c (assoc_attachclasses (uml_assoc umlcd)) -> set_In c (makeclass_name (uml_class umlcd)).

其中函数assoc_attachclasses计算类图中的关联类的类名集合，函数uml_assoc返回类图中的关联关系集合，函数uml_class返回类图中的类的类名集合。

定义10 类图的泛化关系UMLGeneralizetion中的父类和子类名均属于集合UMLClass的类名集合。

Definition UMLCD_post3 (umlcd : UMLClassDiagram) : Prop := forall (c : Class), set_In c (allclasses (uml_gen umlcd)) -> set_In c (makeclass_name (uml_class umlcd)).

函数allclasses计算泛化关系中的父类名和子类名的集合，函数uml_gen返回类图中的泛化关系的集合。

UML类图的形式化定义是满足上述约束的类型为UMLClassDiagram的数据类型：

Definition UMLClassDiagrams := { umlcd : UMLClassDiagram | UMLCD_post1 umlcd ∧ UMLCD_post2 umlcd ∧ UMLCD_post3 umlcd }.

3 精化操作

类图是由所有类、类之间的关系和关系的约束组成的集合，主要体现了需求工程中系统的静态结构。对于类图的精化操作研究，本文主要侧重于系统结构方面的精化操作，即添加、删除或修改类、关联类、关联关系以及泛化关系。类图的精化操作往往是一种迭代过程：给出一个抽象的类图模型，通过一系列复杂的精化操作，最终得到一个具体的类图模型。每个中间模型都必须与其精化后的模型保持一致，即精化前后系统的结构和语义保持一致。本节给出四种类图精化的原子操作，复杂的精化操作可通过有限次的调用原子操作实现:

3.1 添 加

向已有的类图中添加新的类或关联类，函数addumlclass是向给定的类图(UMLClassDiagrams)中添加新的类(umlclass)，其核心是将添加的类定义成umlclass类型并添加到list umlclass的集合中：

Definition addumlclass (u : umlclass) (UCD : UMLClassDiagrams) := match UCD with

| (s, ass, assocclass, gen) => (u :: s, ass, assocclass, gen)

end.

3.2 删 除

从已有的类图中删除指定的类或关联类，分为以下两种情况：

1) 如果删除的对象是关联类c，那么直接删除集合UMLAssocClass中的关联类名为c的元素，包括其关联类和关联端点；

2) 如果删除的对象是集合UMLClass中的一般类，首先搜索关联关系集合、关联类集合和泛化关系集合，如果关联端点或泛化关系中存在该类名，那么先执行拆分操作，删除其关联关系或泛化关系。然后调用函数re_class，通过搜索集合umlclass中是否存在c，如果存在则将其从umlclass中删除。函数removeclass是从给定的类图(UMLClassDiagrams)删除指定的类u。

Fixpoint re_class (c : Class) (u : list umlclass) :=

match u with

| nil => nil

| x :: A => if class_dec c (class_name x) then A else x :: re_class c A

end.

Definition removeclass (u : umlclass) (UCD : UMLClassDiagram) :=

match UCD with

| (s, asso, assocclass, gen) => (re_class (class_name u) s, asso, assocclass, gen)

end.

3.3 链 接

向已有的类图中添加新的关联关系或泛化关系，其Coq定义与添加操作类似。

3.4 拆 分

从已有的类图中删除指定的关联关系或泛化关系，其Coq定义与删除操作类似。

定理1 设u:umlclass, UCD:UMLClassDiagram，如果u不属于集合ClassName并且UCD满足上述类图的形式规约UML_post UCD，那么执行添加操作后得到的类图也满足形式规约UMLCD_post (addClass u UMLCD)：

Theorem add_UML_pre :

forall (u : umlclass) (UCD : UMLClassDiagram),

set_In u (uml_class UCD) ∧ UMLCD_post UCD ->

UMLCD_post (addumlclass u UCD).

定理2 设a:associations, UCD:UMLClassDiagram,如果a不属于类图UCD的关联关系，并且UCD中的所有关联关系a均符合上述形式规约，那么执行链接操作后得到的类图也满足形式规约UMLCD_post (addlink u UMLCD)：

Theorem addlink_UML_pre :

forall (al : associations) (UCD : UMLClassDiagram),

～ set_In u (uml_assoc UCD) ∧ UMLCD_post UCD ->

UMLCD_post (addlink al UCD).

其中函数uml_assoc是返回类图UMLClassDiagram中的关联关系的集合。

上述定理表明：如果类图满足上述的形式规约，那么它执行上述四种精化操作后得到的类图也满足上述形式规约。复杂的类图精化操作可以通过有限次的原子精化操作得到，如添加一个类，首先在UMLClass集合中添加该类的具体信息，然后在执行链接操作将其与该类图中的其他类相关联。对精化操作的原子操作的机械验证，保证了其复杂的精化操作的正确性，从而验证了UML类图精化操作前后的结构和语义的一致性。

4 实例验证

本节给出一个图书馆系统的类图，如图1所示，我们将其转换成上述由定理证明器Coq所描述的形式规约，并且验证该类图符合UML类图的形式化规约。图1包括三个实体类Reader，Copy和Publication。类Publication可以泛化成两个子类Periodical和Book。关联类Loan表示类Reader和类Copy之间的关系，并且具有类Loan。关联关系catalogue将类Copy和类Publication相关联。

根据上述的定义，由于篇幅有限，本文只给出上述类图的部分形式化规约定义：

首先，定义各个类的名字，其类型为Class如class “Loan”表示类名为Loan的类，其次定义每个类的属性与操作集合如property “loaddate”表示属性loaddate，operation “CheckOverdue”表示操作CheckOverdue，类的属性的类型为Property，Loanproperty和Loanoperation分别是类图Loan的属性和操作的集合，LoanClass是将类名Loan到其具体参数LoanDec的映射，BookSysClass表示类的集合。

(* An example of ClassDec *)

Definition Loan := class ″Loan″.

Definition Reader := class ″Reader″.

(* class Loan *)

Definition loaddate := property ″loaddate″.

…

Definition CheckOverdue := operation ″CheckOverdue″.

Definition Loanproperty : list Property := loaddate :: duedate :: nil.

Definition Loanoperation : list Operation := CheckOverdue :: nil.

…

Definition BookDec : ClassDec := (Bookproperty, Peroperation, attrstate, sigos).

(* uml2class *)

Definition LoanClass : umlclass := class2dec Loan LoanDec.

…

Definition BookSysClass : list umlclass := ReaderClass :: CopyClass :: PubClass :: PerClass :: BookClass :: nil.

图1 UML类图的实例

接着，定义类图的关联关系：图1中类Copy与Publication具有关联关系，asscollection表示与类Copy相连接的关联端点，角色名为collection，多重性是0...*，由于Coq的自然数域只是表示有限的数，因此设多重性的最大值为100，附加类是Copy，关联类型为none。coll2detail表示上述关联关系，其关联名为catalogue，关联端点为asscollection和assdetail。关联类与泛化关系与上述类似，不再赘述。

(* assoc *)

Definition asscollection : AssociationEnd := (″collection″, 100, Copy, none).

Definition assdetail : AssociationEnd := (″detail″, 1, Publication, none).

Definition coll2detail : associations := (″catalogue″, (asscollection, assdetail)).

(*assocclass*)

Definition assborrower : AssociationEnd := (″borrower″, 1, Reader, none).

Definition assloanedcopy : AssociationEnd := (″loanedcopy″, 5, Copy, none).

Definition assclassborrowloaned : AssocClassDec := (LoanClass, (assborrower, assloanedcopy)).

(*genalizations*)

Definition subPublish : set Class := Periodical :: Book :: nil.

Definition BookGen : GenDec := (Publication, subPublish) :: nil.

Definition BookClassDiagram : UMLClassDiagrams := (BookSysClass, BookAsso, BookAssoClass, BookGen)

为了说明上述类图是符合类图的形式规约，本文通过验证上述形式化定义满足形式规约命题，由于篇幅有限，只给出定义7的Coq证明过程：

Example UML_post2 :

UMLCD_post2 BookClassDiagram.

Proof.

unfold UMLCD_post2, BookClassDiagram.

simpl; intros. inversion H.

subst. right. left. reflexivity.

inversion H0. subst. right. right.

left. reflexivity.

inversion H1.

Qed.

5 相关工作

将UML和形式化方法相结合是国内外广大学者和科研组织的一个研究热点，目的是弥补半形式化的UML缺乏精确语义定义的不足。目前UML形式化方法有两种思路：一是对UML核心语法进行形式化，使得UML成为符合形式化规范的语言，如英国PUML 工作组在元模型层次(UMLMeta-model)对UML进行形式化，保证在此基础上建立的UML 模型层和用户对象层有可靠的数学模型基础，可对构造、操纵和精化模型提供一种通用的方法。另一种是转换法，利用形式化语言在不丢失或者少丢失信息的前提下对UML进行形式化，如Kim等[5-6]将UML类图转换为Z形式规格说明，然而Kim仅考虑类、类属性、类操作、关联以及泛化的转换，没有考虑模型中的约束条件。

Tanuan[7]、Lano[8]基于Meyer等[9]的部分工作，提出了从UML结构概念到B形式规约的派生方案，将每个类属性、关联和状态模型转换成B变量，类之间的关系形式化为代表类的变量的谓词不变式。Cali[10]使用描述逻辑(Description Logics)对UML类图进行形式化描述。Szlenk[11]定义了类图的形式语义，并且介绍了类图中的一致性问题。Anastasakis[12]将带OCL约束的UML自动转换到Alloy代码。黄春荣等[15]给出了UML模型到COOZ规约的一种系统转换方法，用COOZ类形式化描述类图中的元素语法和语义。杨敬中等[16]提出了用XYZ/E来描述UML类图的形式化语言，XYZ/E是一种面向软件开发全过程的时序逻辑语言，既能表示软件系统的规范与性质，又能表示软件系统的数学模型与程序实现。

6 结 语

本文从类图的形式语义中抽取出形式规约，使用定理证明器Coq描述UML类图的形式规约，提出了UML类图的结构精化操作，并且在Coq中对其进行形式化描述。基于上述的形式规约，UML类图和精化操作的重要属性转换为数学定理，在Coq中形式描述并机械验证。此外，本文通过一个小型的类图实例表明了上述形式规约的可行性与正确性。与之前的UML序列图和状态图的机械验证相结合，为提出可验证的软件设计模型精化框架提供理论基础。

基于现有工作，我们将从以下方面做进一步研究：(1)添加UML类图的OCL约束的形式化定义，使得带OCL约束的UML类图能够形式化描述；(2)使用Kermeta转换工具，实现从UML类图转换到Coq定义的形式化描述的自动化转换工具；(3)实现包括类图、序列图和状态图的可验证软件设计模型精化框架。

[1] Evans A S.Reasoning with UML class diagrams[C]//Proceedings of the 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques.IEEE Press,1998:102-113.

[2] Rational Software Corporation.UML Notation Guide Version 1.1[OL].http://www.rational.com.

[3] The Coq System[OL].http://coq.inria.fr/.

[4] Dou L,Lu L,Yang Z,et al.Towards mechanized semantics of UML sequence diagrams and refinement relation[C]//Proceedings of the 24th IASTED International Conference on Modelling and Simulation,2013:262-269.

[5] Kim S K,Carrington D.An integrated framework with UML and Object-Z for developing a precise and understandable specification: the light control case study[C]//Proceedings of the 7th Asia-Pacific Software Engineering Conference,2000:240-248.

[6] Kim S K,Carrington D.Formalizing the UML class diagram using Object-Z[C]//Proceedings of the 2nd International Conference on The Unified Modeling Language:Beyond the Standard,Fort Collins,CO,USA,1999:83-98.

[7]TanuanMC.Automatedanalysisofunifiedmodelinglanguage(UML)specifications[D].Waterloo,Ontario,Canada:UniversityofWaterloo,2001.

[8]LanoK,ClackD,AndroutsopoulosK.UMLtoB:formalverificationofobject-orientedmodels[C]//Proceedingsofthe4thInternationalConferenceonIntegratedFormalMethod,2004:187-206.

[9]MeyerE,SouquièresJ.AsystematicapproachtotransformOMTdiagramstoaBspecification[C]//ProceedingsoftheWorldCongressonFormalMethodsintheDevelopmentofComputingSystems.Springer,1999:875-895.

[10]CalìA,CalvaneseD,GiacomoGD,etal.AformalframeworkforreasoningonUMLclassdiagrams[C]//Proceedingsofthe13thInternationalSymposiumonFoundationsofIntelligentSystems.Springer,2002:503-513.

[11]SzlenkM.FormalsemanticsandreasoningaboutUMLclassdiagram[C]//DependabilityofComputerSystems,2006InternationalConferenceon.IEEE,2006:51-59.

[12]AnastasakisK,BordbarB,GeorgG,etal.UML2Alloy:achallengingmodeltransformation[C]//Proceedingsofthe10thinternationalconferenceonModelDrivenEngineeringLanguagesandSystems.Springer,2007:436-450.

[13]UniversityofCambridge.Isabelle[OL].http://isabelle.in.tum.de.

[14]Wikipedia.Kermeta[DB/OL].https://en.wikipedia.org/wiki/Kermeta.

[15] 黄春荣,李宣东,郑国梁.UML模型到COOZ规约的形式化转换[J].计算机工程与应用,2003,39(20):89-91.

[16] 杨敬中,张广泉,戎玫.UML2.0类图的一种形式化描述方法[J].计算机科学,2007,34(2):277-279,288.

FORMAL SPECIFICATION AND REFINEMENT FOR UML CLASS DIAGRAM

Wang Bowen Sheng Feng Dou Liang Yang Zongyuan

(SchoolofInformationScienceandTechnology,EastChinaNormalUniversity,Shanghai200241,China)

The Unified Modeling Language (UML) is an important part of Modeling-driven engineering (MDE) because of its variety of well-known and intuitive graphical notations. However, the semantics of UML is not precisely defined and the correctness of refinements cannot be verified, which makes it difficult to verify in formal of the UML model. As the static model of describing system structure, UML class diagram has no complete formal semantics. Thus, using the theorem proof assistant Coq to formalize and mechanize the semantics of the UML class diagram and the refinements between the models. The syntactic structure and the semantics of the UML class diagram can be transformed to the rigorous definitions in Coq, which is called mechanized semantics. Besides, the structural refinement operations of the class diagram are also provided. The refinement relations between models can be formally defined in Coq, and the desired properties of the refinement relations can be proven to verify the correctness of the refinements, ensuring the consistency of structure and semantics before and after refining. Combining the UML and formal method, the theoretical foundation in the software developing process is provided.

UML class diagram Model refinement Coq Mechanized semantics

2016-01-15。国家自然科学基金项目(61070226)。王博文，硕士生，主研领域：UML和软件形式化验证。盛枫，博士生。窦亮，讲师。杨宗源，教授。

TP301.2

A

10.3969/j.issn.1000-386x.2017.02.001