基于矩阵理论的UML类图形式化描述与检测
2017-06-28王智广李聪莹
王智广，王 雷，李聪莹
(1 中国矿业大学(北京) 机电与信息工程学院，北京 100083；2 中国石油大学(北京) 地球物理与信息工程学院，北京 102249)
基于矩阵理论的UML类图形式化描述与检测
王智广1，2，王 雷1,*，李聪莹2
(1 中国矿业大学(北京) 机电与信息工程学院，北京 100083；2 中国石油大学(北京) 地球物理与信息工程学院，北京 102249)
针对UML缺少形式化语义，使得开发UML自动检测工具变得困难的问题，提出了一种基于矩阵理论的UML类图形式化描述和自动检测方法.首先，分别给出了基于二元关系和基于矩阵的类图形式化描述规则；然后，讨论了UML类图的自动检测；最后，用一个实例说明了该方法的有效性.实验结果表明：该方法可以对UML类图进行形式化描述，且可以通过数学方法找出模型中存在的错误.
二元关系；矩阵；UML类图；形式化描述；检测
UML(统一建模语言)作为一种面向对象分析和设计的建模语言已被用在很多大型软件系统中.如今UML模型的复杂性变得越来越高，对所建立的模型进行正确性检测变得很有必要[1].近年来，国内外的学者提出了很多不同的UML模型形式化和检测方法.一些文献采用目前已有的比较成熟的形式化建模语言对UML模型进行形式化.文献[2-5]将Petri网用于UML模型的形式化.笔者在之前的研究中[6]也曾采用Petri网对UML进行形式化建模.这些方法既可以形式化UML静态模型，又可以形式化UML动态模型.然而，比起UML模型，Petri网更适合于对并发系统建模.文献[7-9]采用π演算来描述UML模型.π演算有着严格的语法和推演规则，可以对UML模型进行精确描述和严格检测.然而，π演算无法用图形符号形象地将UML模型展现出来，而且其规约过程较为复杂，给自动检测算法的实现带来困难.文献[10]提出了一种通过中间模型将UML模型转换为马尔科夫链的方法.该方法使得可靠性分析工作变得更加方便、高效.但是该方法的转换过程非常复杂，使得开发自动化支持工具变得困难.还有一些学者提出了一些新的形式化语言对UML进行形式化.文献[11]给出了一种新的形式化语言 (PUML) .该语言对UML模型的语义具有完备、准备的表达.但是因为该语言的理论还不够成熟，难以对UML模型进行进一步处理，所以文献[11]仅仅给出了基于PUML的UML模型描述规则.将UML进行形式化描述的目的在于对模型进行检测和分析，仅仅给出描述规则意义不大.文献[12]给出了一种UML形式化描述语言(UML-B).该语言可以增强UML模型的复用性，且可以通过严格的数学方法对模型进行检测.然而，该语言无法对UML模型进行精确的描述.精确的描述是有效检测UML模型的基础，所以该方法的检测结果并不完全可靠.文献[13,14]实现了UML类图和顺序图的自动检测, 但是这些方法是基于UML本身的, 所以这些方法的检测准确度不高.
根据UML类图的特点，本文提出一种基于二元关系和矩阵的UML类图形式化描述和检测方法.该方法具有以下一些优势.
(1) 形式化描述规则和自动检测算法较为简单.
(2) 类图的二元关系和矩阵表示保留了原模型的全部语义.
(3) 该方法既可以对UML类图进行精确描述，又可以对类图进行检测.在此基础上，可以较为容易地实现相应的自动化软件工具.
1 相关理论基础
1.1UML类图及类的关系
UML类图描述类以及类之间的静态关系.类图是一种静态模型，它是创建其他UML图的基础.UML中类的图形符号为长方形，有两条横线把长方形分为上、中、下三个区域，三个区域分别放类的名字、属性和服务.
在类图中，类与类之间的关系主要有4种：关联、泛化、依赖和聚合[15].在关联关系中，被关联类以类的属性的形式出现在关联类中.泛化关系又称为继承关系.一个类可以继承另一个类的全部属性和操作，此外，还可以定义自己特有的属性和操作.前者称为后者的特殊类(子类)，后者称为前者的一般类(父类)，两者之间的关系称为泛化关系.在依赖关系中，引用类作为参数出现在使用类中.聚合关系是一种特殊的关联关系，表示的是整体与部分的关系.关系的图形表示如图1所示.
a) 关联关系；b) 泛化关系；c) 依赖关系；d) 聚合关系图1 关系的图形表示Fig.1 Graphic symbol of relationships
此外，类的操作之间还存在调用关系.若一个操作调用另一个操作，则称前者为主调操作，后者为被调操作.
1.2 关系的定义及其运算
本文所提出的UML类图形式化描述和检测方法建立在关系理论[16]基础之上.下面给出关系的相关概念.
定义1 如果一个集合中的元素都是有序对或者这个集合是空集，则称这个二元集合是一个二元关系，简称关系.关系的名字一般使用大写的英文字母，通常记作R.
A与B的笛卡尔积A×B的任何子集所定义的二元关系叫做从A到B的二元关系，当A=B时则叫做A上的二元关系.
定义2 设R，S为二元关系，R与S的合成记作R∘S，则：
R∘S={
可以使用关系矩阵来表示二元关系.关系矩阵的定义如下：
定义3 设A={x1,x2,…,xn}，B={y1,y2,…,ym}，R是A到B的关系，R的关系矩阵是布尔矩阵：
MR=(rij)n×m，
其中rij=1⟺
当R为A上的关系时，R的关系矩阵是n阶方阵.
计算关系的合成可以利用关系矩阵的乘法.设R和S的关系矩阵为MR和MS，R∘S的关系矩阵为MR∘S，则：
MR∘S=MRMS.
2 UML类图的形式化描述
对UML类图进行形式化描述是自动检测的基础.设G为一个类图，下面分别给出基于二元关系和基于矩阵的UML类图形式化描述规则.
2.1 基于二元关系的UML类图形式化描述
上文给出了关系的定义及其运算.在UML类图中，类和类之间存在关系，而属性、操作和类三者之间也存在关系.下面给出类图的二元关系描述规则.
类图G可以表示为一个11元组：
G=(C,A,O,RAss,RGen,RDep,RC-A,RC-O,RO-O,RA-C,RO-C),
其中：
(1)C={c1,c2,…,cn}为G的所有类的集合.
(2)A={a1,a2,…，am}为G的所有属性的集合.
(3)O={o1,o2,…,op}为G的所有操作的集合.
(4)RAss⊆(C×C)为C上的二元关系.
(5)RGen⊆(C×C)为C上的二元关系.
(6)RDep⊆(C×C)为C上的二元关系.
(7)RC-A⊆(C×A)为从C到A的二元关系.
(8)RC-O⊆(C×O)为从C到O的二元关系.
(9)RO-O⊆(O×O)为O上的二元关系.
(10)RA-C⊆(A×C)为从A到C的二元关系.
(11)RO-C⊆(O×C)为从O到C的二元关系.
为了区分属于不同类的同名属性和操作，采用以下格式来表示属性和操作：
类名::属性名
类名::操作名
2.2 基于矩阵的UML类图形式化描述
UML类图也可以用矩阵来形式化描述.下面给出类图G的关系矩阵的定义.
定义6G的关联关系矩阵定义为布尔矩阵：
MAss=(rij)n×m,
其中rij=1⟺
类似可以得到泛化关系矩阵MGen和依赖关系矩阵MDep的定义.G的关联关系矩阵、泛化关系矩阵和依赖关系矩阵均为n阶方阵，其中n为G中类的个数.
定义7G的属性从属关系矩阵定义为：
MC-A=(rij)n×m,
其中rij=1⟺
类似地可以定义G的操作从属关系矩阵MC-O.
定义8G的调用关系矩阵定义为：
MO-O=(rij)p×p,
其中rij=1⟺
和类关系矩阵类似，G的调用关系矩阵为一个p阶方阵，其中p为网中所有操作的个数.
定义9 类图G的属性类型矩阵定义为.
MA-C=(rij)m×n,
其中rij=1⟺
类似地可以定义G的操作类型矩阵MO-C.
3 UML类图的自动检测
将UML类图形式化描述后，就能够采用数学的方法对类图的正确性进行自动检测[17].下面给出几种常见错误的检测定理.
在建模过程中，建模人员可能会将关联关系错误地定义为别的关系，或者漏掉某个属性.设G为一个类图，下面给出关联关系的检测定理.
定理1 设MC-AMA-C=(rij)n×n，MAss=(sij)n×n.若MC-AMA-C≠MAss，则G存在关联关系错误.分以下两种情况：
(1) 若rij=1且sij=0，则类ci与类cj之间的关系定义错误(应为关联关系而非其他关系).
(2) 若rij=0且sij=1，则类ci漏掉类型为cj的属性.
类似地，在建模过程中，建模人员可能会将依赖关系错误地定义为别的关系，或者漏掉某个操作.下面给出依赖关系的检测定理.
定理2 设MC-OMO-C=(rij)n×n，MDep=(sij)n×n.若MC-OMO-C≠MDep，.则G存在依赖关系错误.分以下两种情况：
(1) 若rij=1且sij=0，则类ci与类cj之间的关系定义错误(应为依赖关系而非其他关系).
(2) 若rij=0且sij=1，则类ci漏掉参数类型为cj的操作.
在UML类图中，类之间不能存在递归泛化[18].用图形符号表示，即不能出现环状的泛化关系.下面给出检测UML类图中是否存在递归泛化的定理.
在UML类图中，泛化的深度不宜过大.下面给出检测UML类图的泛化深度的定理.
在实际的UML类图检测过程中，一般首先规定一个最大深度.得到类图的泛化深度后，可以判断该深度是否超过该最大深度.
这里不给出以上定理的严格证明过程.后面将以一个具体的UML类图形式化描述和检测实例说明上述定理的有效性.
4 UML类图形式化描述和检测实例
下面给出一个基于二元关系和矩阵的UML类图形式化描述和检测实例.
图2为一个在线学习系统[19]的UML类图片段.设该UML类图为G.
图2 在线学习系统的UML类图片段Fig.2 UML Class Diagram Fragment of an Online Learning System
4.1 答题系统类图的形式化描述
记c1 =Chapter，c2 =Excercise，c3 =Completion，c4 =TrueOrFalseQuestion，c5 =Choice，c6 =SingleChoice，c7 =MultipleChoice;a1=Chapter::chapterNo，a2=Chapter::socre，a3=Chapter::excericise，a4=Excercise::excericisNo，a5=Completion::answer，a6=TrueOrFalseQuestion::answer，a7=SingleChoice::answer，a8=MultipleChoice::answer;o1=Chapter::DoExcericise,o2=Chapter::UpdataScore，o3=Excercise::IsRight,o4=Completion::IsRight,o5=TrueOrFalseQuestion::IsRight,o6=Choice::IsRight,o7=SingleChoice::IsRight,o8=MultipleChoice::IsRight.则类图G可以表示为一个11元组：
G=(C,A,O,RAss,RGen,RDep,RC-A,RC-O,RO-O,RA-C,RO-C),
其中：
(1)C={c1,c2,…,c7}.
(2)A={a1,a2,…,a8}.
(3)O={o1,o2,…,o8}.
(4)RAss={}=Φ.
(5)RGen={
(6)RDep={
(7)RC-A={
(8)RC-O={
(9)RO-O={
(10)RA-C={
(11)RO-C={}=Φ.
类图G也可以用矩阵来形式化描述.下面的模型检测过程将会用到属性从属关系矩阵MC-A、属性类型矩阵MA-C、关联关系矩阵MAss和泛化关系矩阵MGen，所以这里只给出这几个矩阵.根据定义，可得：
4.2 答题系统类图的检测
这里给出检测的原理，在后续的研究中将设计并实现UML类图自动检测工具.
(1) 关联关系的检测.
经计算可知，
显然MC-AMA-C≠MAss，由定理1可知类图G存在关联关系错误.
而r12=1且s12=0，由定理1(1)可知类c1与类c2之间的关系定义错误 (应为关联关系而非其他关系).
由图2所示UML类图可知，类Chapter包含类型为Exercise的属性exercise，而类Chapter和类Exercise之间的关系却错误地定义为泛化关系.由此可见，定理1可以准确地检测出类图中存在的关联关系错误.
(2) 递归泛化的检测.
由图2所示UML类图易见类Exercise、类Choice和类MultipleChoice之间的泛化关系为一个环状，亦即模型存在递归泛化.
将类图G进行修改，去掉类Exercise继承于类MultipleChoice的泛化关系，如图3所示.设该类图为G′.
图3 修改后的UML模型Fig.3 Modified UML Class Diagram
此时,
综上所述，定理4可以有效地检测出类图中的递归泛化.
(3) 泛化深度的检测.
由图3所示UML类图易见泛化深度为2.由此可见，定理4可以准确地检测出类图的泛化深度.
5 结论
UML模型的形式化描述和自动检测是当前计算机领域的一个研究热点.本文提出的UML类图形式化描述和检测方法既具有完全形式化的图形表示方法，又有坚实的数学理论支撑.该方法借助了关系理论和矩阵理论，可以进一步开发自动化工具对模型进行严格地检查和分析.本文提出的方法仍存在一些缺陷.下一步的研究工作将从以下几个方面展开.
(1) 为了设计出高质量的软件，设计过程需要遵循一定的设计原则[20].如何根据这些原理对所设计的UML类图进行自动优化是下一步的研究重点.
(2) 目前只得到UML类图的形式化描述与检测方法.在今后的研究中将对该方法进行拓展，使其可以对UML的其他几种图进行形式化描述和检测.
(3) 目前只得了几种常见错误的检测定理.在今后的工作中将进一步完善正确性检测定理.
(4) 设计并实现UML类图自动检测工具也是下一步研究的重点.
[1] Hammal Y. A formal methodology for semantics and time consistency checking of UML dynamic diagrams [J]. Journal of the Chinese Institute of Engineers, 2009, 34(2):197-211.
[2] Arcaini P, Gargantini A, Riccobene E, et al. A model-driven process for engineering a toolset for a formal method [J]. Software Practice & Experience, 2011, 41(2):155-166.
[3] Choppy C, Klai K, Zidani H. Formal verification of UML state diagrams: a petri net based approach [J]. Acm Sigsoft Software Engineering Notes, 2011, 36(1):1-8.
[4] Talouki R N, Motameni H. Modeling sequence diagram in Fuzzy Uml to Fuzzy Petri-net for calculating reliability parameter [J]. Research Journal of Applied Sciences Engineering & Technology, 2013, 6(20).
[5] 赵俊峰, 周建涛, 邢冠男. UML活动图到Petri网的转换方法及实现研究[J]. 计算机科学, 2014, 41(7):143-147.
[6] 王 雷, 姜久雷, 王晓峰. 基于Petri网的设计模式形式化描述[J]. 计算机工程, 2016, 42(7): 33-36.
[7] Belghiat A, Chaoui A, Maouche M, et al. Formalization of mobile UML statechart diagrams using the π -calculus: an approach for modeling and analysis[J]. Communications in Computer & Information Science, 2014, 465:236-247.
[8] Dingel J, Paen E, Posse E, et al. Definition and implementation of a semantic mapping for UML-RT using a timed pi-calculus[C]// ACM. International Workshop on Behaviour Modelling. USA: ACM, 2010:1-8.
[9] Belghiat A. Formalization of UML Communication Diagrams using π-Calculus[C]// University of Souk Ahras. Symposium of Complex Systems and Intelligent Computing. Algeria: University of Souk Ahras. 2015:12-17.
[10] 柳 毅, 麻志毅, 何 啸,等. 一种从UML模型到可靠性分析模型的转换方法[J]. 软件学报, 2010, 21(2): 287-304.
[11] Evans A, France R, Lano K, et al. Developing the UML as a formal modelling notation[J]. Computer Science, 2014, 19(98):297--307.
[12] Snook C, Savicks V, Butler M. Verification of UML models by translation to UML-B [J]. Formal Methods for Components & Objects, 2011, 6957:251.
[13] Chavez H M, Shen W, France R B, et al. An approach to checking consistency between UML class model and its Java implementation[J]. IEEE Transactions on Software Engineering, 2016, 42(4):322-344.
[14] Ekanayake EMNK, Kodituwakku SR. Consistency checking of UML class and sequence diagrams [C]// IEEE. International Conference on Ubi-Media Computing. Brazil:IEEE, 2015:24-31.
[15] Vieweg I, Werner C, Wagner K P, et al. Unified modeling language (UML) [M]. Wiesbaden: Gabler Verlag, 2012:367-377.
[16] Merris R. Wiley-Interscience series in discrete mathematics and optimization [M]. New Jersey: John Wiley & Sons, 2011:409-419.
[17] Choi J, Jee E, Bae D H. Timing consistency checking for UML/MARTE behavioral models [J]. Software Quality Journal, 2016, 24(3):835-876.
[18] Herchi H, Abdessalem W B. From user requirements to UML class diagram [J]. Computer Science, 2012.
[19] Griff E R, Matter S F. Evaluation of an adaptive online learning system [J]. British Journal of Educational Technology, 2013, 44(1):170-176.
[20] 杨放春，龙湘明.软件非功能属性研究[J].北京邮电大学学报，2004，27(3)：1-12.
Formal Description and Checking of UML Class Diagram Based on Matrix Theory
WangZhiguang1，2，WangLei1，LiCongying2
(1 School of Mechanical Electronic & Information Engineering, China University of Mining & Technology (Beijing), Beijing 100083, China;2 College of Geophysics and Information Engineering, China University of Petroleum (Beijing), Beijing 102249, China)
UML lacks formal semantics, making it difficult to develop UML automatic checking tools, so a formal description and automatic checking method of UML class diagram based on matrix theory was proposed. First, the formal description rules of class diagram based on binary relation and matrix was given respectively. Then, the automatic checking of UML class diagram was discussed. Finally, the effectiveness of this method was illustrated by an instance. Experimental results show that this method can describe the UML class diagram formally, and can find out the errors exist in the model through mathematical methods.
binary relation；matrix；UML class diagram；formal description；checking
2016-12-16
王智广(1964-)，男，教授，博导，研究方向：软件工程、并行计算，E-mail：wy8952@sohu.com
国家自然科学基金资助项目(60803159)，国家“973”计划项目(2013CB228602))
TP312
A
1672-4321(2017)02-0109-06
*通讯作者 王 雷，研究方向：形式化开发方法、软件体系结构，E-mail: wanglei0823@foxmail.com
