王智廣，王 雷，李聰瑩

(1 中國礦業(yè)大學(xué)(北京) 機(jī)電與信息工程學(xué)院，北京 100083；2 中國石油大學(xué)(北京) 地球物理與信息工程學(xué)院，北京 102249)

基于矩陣?yán)碚摰腢ML類圖形式化描述與檢測(cè)

王智廣1，2，王 雷1,*，李聰瑩2

(1 中國礦業(yè)大學(xué)(北京) 機(jī)電與信息工程學(xué)院，北京 100083；2 中國石油大學(xué)(北京) 地球物理與信息工程學(xué)院，北京 102249)

針對(duì)UML缺少形式化語義，使得開發(fā)UML自動(dòng)檢測(cè)工具變得困難的問題，提出了一種基于矩陣?yán)碚摰腢ML類圖形式化描述和自動(dòng)檢測(cè)方法.首先，分別給出了基于二元關(guān)系和基于矩陣的類圖形式化描述規(guī)則；然后，討論了UML類圖的自動(dòng)檢測(cè)；最后，用一個(gè)實(shí)例說明了該方法的有效性.實(shí)驗(yàn)結(jié)果表明：該方法可以對(duì)UML類圖進(jìn)行形式化描述，且可以通過數(shù)學(xué)方法找出模型中存在的錯(cuò)誤.

二元關(guān)系；矩陣；UML類圖；形式化描述；檢測(cè)

UML(統(tǒng)一建模語言)作為一種面向?qū)ο蠓治龊驮O(shè)計(jì)的建模語言已被用在很多大型軟件系統(tǒng)中.如今UML模型的復(fù)雜性變得越來越高，對(duì)所建立的模型進(jìn)行正確性檢測(cè)變得很有必要[1].近年來，國內(nèi)外的學(xué)者提出了很多不同的UML模型形式化和檢測(cè)方法.一些文獻(xiàn)采用目前已有的比較成熟的形式化建模語言對(duì)UML模型進(jìn)行形式化.文獻(xiàn)[2-5]將Petri網(wǎng)用于UML模型的形式化.筆者在之前的研究中[6]也曾采用Petri網(wǎng)對(duì)UML進(jìn)行形式化建模.這些方法既可以形式化UML靜態(tài)模型，又可以形式化UML動(dòng)態(tài)模型.然而，比起UML模型，Petri網(wǎng)更適合于對(duì)并發(fā)系統(tǒng)建模.文獻(xiàn)[7-9]采用π演算來描述UML模型.π演算有著嚴(yán)格的語法和推演規(guī)則，可以對(duì)UML模型進(jìn)行精確描述和嚴(yán)格檢測(cè).然而，π演算無法用圖形符號(hào)形象地將UML模型展現(xiàn)出來，而且其規(guī)約過程較為復(fù)雜，給自動(dòng)檢測(cè)算法的實(shí)現(xiàn)帶來困難.文獻(xiàn)[10]提出了一種通過中間模型將UML模型轉(zhuǎn)換為馬爾科夫鏈的方法.該方法使得可靠性分析工作變得更加方便、高效.但是該方法的轉(zhuǎn)換過程非常復(fù)雜，使得開發(fā)自動(dòng)化支持工具變得困難.還有一些學(xué)者提出了一些新的形式化語言對(duì)UML進(jìn)行形式化.文獻(xiàn)[11]給出了一種新的形式化語言 (PUML) .該語言對(duì)UML模型的語義具有完備、準(zhǔn)備的表達(dá).但是因?yàn)樵撜Z言的理論還不夠成熟，難以對(duì)UML模型進(jìn)行進(jìn)一步處理，所以文獻(xiàn)[11]僅僅給出了基于PUML的UML模型描述規(guī)則.將UML進(jìn)行形式化描述的目的在于對(duì)模型進(jìn)行檢測(cè)和分析，僅僅給出描述規(guī)則意義不大.文獻(xiàn)[12]給出了一種UML形式化描述語言(UML-B).該語言可以增強(qiáng)UML模型的復(fù)用性，且可以通過嚴(yán)格的數(shù)學(xué)方法對(duì)模型進(jìn)行檢測(cè).然而，該語言無法對(duì)UML模型進(jìn)行精確的描述.精確的描述是有效檢測(cè)UML模型的基礎(chǔ)，所以該方法的檢測(cè)結(jié)果并不完全可靠.文獻(xiàn)[13,14]實(shí)現(xiàn)了UML類圖和順序圖的自動(dòng)檢測(cè), 但是這些方法是基于UML本身的, 所以這些方法的檢測(cè)準(zhǔn)確度不高.

根據(jù)UML類圖的特點(diǎn)，本文提出一種基于二元關(guān)系和矩陣的UML類圖形式化描述和檢測(cè)方法.該方法具有以下一些優(yōu)勢(shì).

(1) 形式化描述規(guī)則和自動(dòng)檢測(cè)算法較為簡單.

(2) 類圖的二元關(guān)系和矩陣表示保留了原模型的全部語義.

(3) 該方法既可以對(duì)UML類圖進(jìn)行精確描述，又可以對(duì)類圖進(jìn)行檢測(cè).在此基礎(chǔ)上，可以較為容易地實(shí)現(xiàn)相應(yīng)的自動(dòng)化軟件工具.

1 相關(guān)理論基礎(chǔ)

1.1UML類圖及類的關(guān)系

UML類圖描述類以及類之間的靜態(tài)關(guān)系.類圖是一種靜態(tài)模型，它是創(chuàng)建其他UML圖的基礎(chǔ).UML中類的圖形符號(hào)為長方形，有兩條橫線把長方形分為上、中、下三個(gè)區(qū)域，三個(gè)區(qū)域分別放類的名字、屬性和服務(wù).

在類圖中，類與類之間的關(guān)系主要有4種：關(guān)聯(lián)、泛化、依賴和聚合[15].在關(guān)聯(lián)關(guān)系中，被關(guān)聯(lián)類以類的屬性的形式出現(xiàn)在關(guān)聯(lián)類中.泛化關(guān)系又稱為繼承關(guān)系.一個(gè)類可以繼承另一個(gè)類的全部屬性和操作，此外，還可以定義自己特有的屬性和操作.前者稱為后者的特殊類(子類)，后者稱為前者的一般類(父類)，兩者之間的關(guān)系稱為泛化關(guān)系.在依賴關(guān)系中，引用類作為參數(shù)出現(xiàn)在使用類中.聚合關(guān)系是一種特殊的關(guān)聯(lián)關(guān)系，表示的是整體與部分的關(guān)系.關(guān)系的圖形表示如圖1所示.

a) 關(guān)聯(lián)關(guān)系；b) 泛化關(guān)系；c) 依賴關(guān)系；d) 聚合關(guān)系圖1 關(guān)系的圖形表示Fig.1 Graphic symbol of relationships

此外，類的操作之間還存在調(diào)用關(guān)系.若一個(gè)操作調(diào)用另一個(gè)操作，則稱前者為主調(diào)操作，后者為被調(diào)操作.

1.2 關(guān)系的定義及其運(yùn)算

本文所提出的UML類圖形式化描述和檢測(cè)方法建立在關(guān)系理論[16]基礎(chǔ)之上.下面給出關(guān)系的相關(guān)概念.

定義1 如果一個(gè)集合中的元素都是有序?qū)蛘哌@個(gè)集合是空集，則稱這個(gè)二元集合是一個(gè)二元關(guān)系，簡稱關(guān)系.關(guān)系的名字一般使用大寫的英文字母，通常記作R.

A與B的笛卡爾積A×B的任何子集所定義的二元關(guān)系叫做從A到B的二元關(guān)系，當(dāng)A=B時(shí)則叫做A上的二元關(guān)系.

定義2 設(shè)R，S為二元關(guān)系，R與S的合成記作R°S，則：

R°S={|?y(∈R^∈S)}.

可以使用關(guān)系矩陣來表示二元關(guān)系.關(guān)系矩陣的定義如下：

定義3 設(shè)A={x1,x2,…,xn}，B={y1,y2,…,ym}，R是A到B的關(guān)系，R的關(guān)系矩陣是布爾矩陣：

MR=(rij)n×m，

其中rij=1?∈R,i=1,2,…,n,j=1,2,…,m..

當(dāng)R為A上的關(guān)系時(shí)，R的關(guān)系矩陣是n階方陣.

計(jì)算關(guān)系的合成可以利用關(guān)系矩陣的乘法.設(shè)R和S的關(guān)系矩陣為MR和MS，R°S的關(guān)系矩陣為MR°S，則：

MR°S=MRMS.

2 UML類圖的形式化描述

對(duì)UML類圖進(jìn)行形式化描述是自動(dòng)檢測(cè)的基礎(chǔ).設(shè)G為一個(gè)類圖，下面分別給出基于二元關(guān)系和基于矩陣的UML類圖形式化描述規(guī)則.

2.1 基于二元關(guān)系的UML類圖形式化描述

上文給出了關(guān)系的定義及其運(yùn)算.在UML類圖中，類和類之間存在關(guān)系，而屬性、操作和類三者之間也存在關(guān)系.下面給出類圖的二元關(guān)系描述規(guī)則.

類圖G可以表示為一個(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上的二元關(guān)系.表示類c1和類c2之間存在關(guān)聯(lián)關(guān)系，其中c1為關(guān)聯(lián)類，c2為被聯(lián)系類.聚合關(guān)系是一種特殊的關(guān)聯(lián)關(guān)系，所以該關(guān)系包含聚合關(guān)系.

(5)RGen?(C×C)為C上的二元關(guān)系.表示類c1和類c2之間存在泛化關(guān)系，其中c1為一般類，c2為特殊類.

(6)RDep?(C×C)為C上的二元關(guān)系.表示類c1和類c2之間存在依賴關(guān)系，其中c1為使用類，c2為引用類.

(7)RC-A?(C×A)為從C到A的二元關(guān)系.表示屬性a是屬于類c的屬性.

(8)RC-O?(C×O)為從C到O的二元關(guān)系.表示操作o是屬于類c的操作.

(9)RO-O?(O×O)為O上的二元關(guān)系.表示操作o1和操作o2之間存在調(diào)用關(guān)系，其中o1為主調(diào)操作，o2為被調(diào)操作.

(10)RA-C?(A×C)為從A到C的二元關(guān)系.表示屬性a的類型為類c.

(11)RO-C?(O×C)為從O到C的二元關(guān)系.表示操作o的某個(gè)參數(shù)的類型為類c.

為了區(qū)分屬于不同類的同名屬性和操作，采用以下格式來表示屬性和操作：

類名::屬性名

類名::操作名

2.2 基于矩陣的UML類圖形式化描述

UML類圖也可以用矩陣來形式化描述.下面給出類圖G的關(guān)系矩陣的定義.

定義6G的關(guān)聯(lián)關(guān)系矩陣定義為布爾矩陣：

MAss=(rij)n×m,

其中rij=1?∈RAss,i=1,2,…，n.

類似可以得到泛化關(guān)系矩陣MGen和依賴關(guān)系矩陣MDep的定義.G的關(guān)聯(lián)關(guān)系矩陣、泛化關(guān)系矩陣和依賴關(guān)系矩陣均為n階方陣，其中n為G中類的個(gè)數(shù).

定義7G的屬性從屬關(guān)系矩陣定義為：

MC-A=(rij)n×m,

其中rij=1?∈RC-A,i=1,2,…,n,j=1,2,…,m.

類似地可以定義G的操作從屬關(guān)系矩陣MC-O.

定義8G的調(diào)用關(guān)系矩陣定義為：

MO-O=(rij)p×p,

其中rij=1?∈RO-O,i=1,2,…,p,j=1,2,…,p.

和類關(guān)系矩陣類似，G的調(diào)用關(guān)系矩陣為一個(gè)p階方陣，其中p為網(wǎng)中所有操作的個(gè)數(shù).

定義9 類圖G的屬性類型矩陣定義為.

MA-C=(rij)m×n,

其中rij=1?∈RA-C,i=1,2,…,m,j=1,2,…,n.

類似地可以定義G的操作類型矩陣MO-C.

3 UML類圖的自動(dòng)檢測(cè)

將UML類圖形式化描述后，就能夠采用數(shù)學(xué)的方法對(duì)類圖的正確性進(jìn)行自動(dòng)檢測(cè)[17].下面給出幾種常見錯(cuò)誤的檢測(cè)定理.

在建模過程中，建模人員可能會(huì)將關(guān)聯(lián)關(guān)系錯(cuò)誤地定義為別的關(guān)系，或者漏掉某個(gè)屬性.設(shè)G為一個(gè)類圖，下面給出關(guān)聯(lián)關(guān)系的檢測(cè)定理.

定理1 設(shè)MC-AMA-C=(rij)n×n，MAss=(sij)n×n.若MC-AMA-C≠M(fèi)Ass，則G存在關(guān)聯(lián)關(guān)系錯(cuò)誤.分以下兩種情況：

(1) 若rij=1且sij=0，則類ci與類cj之間的關(guān)系定義錯(cuò)誤(應(yīng)為關(guān)聯(lián)關(guān)系而非其他關(guān)系).

(2) 若rij=0且sij=1，則類ci漏掉類型為cj的屬性.

類似地，在建模過程中，建模人員可能會(huì)將依賴關(guān)系錯(cuò)誤地定義為別的關(guān)系，或者漏掉某個(gè)操作.下面給出依賴關(guān)系的檢測(cè)定理.

定理2 設(shè)MC-OMO-C=(rij)n×n，MDep=(sij)n×n.若MC-OMO-C≠M(fèi)Dep，.則G存在依賴關(guān)系錯(cuò)誤.分以下兩種情況：

(1) 若rij=1且sij=0，則類ci與類cj之間的關(guān)系定義錯(cuò)誤(應(yīng)為依賴關(guān)系而非其他關(guān)系).

(2) 若rij=0且sij=1，則類ci漏掉參數(shù)類型為cj的操作.

在UML類圖中，類之間不能存在遞歸泛化[18].用圖形符號(hào)表示，即不能出現(xiàn)環(huán)狀的泛化關(guān)系.下面給出檢測(cè)UML類圖中是否存在遞歸泛化的定理.

在UML類圖中，泛化的深度不宜過大.下面給出檢測(cè)UML類圖的泛化深度的定理.

在實(shí)際的UML類圖檢測(cè)過程中，一般首先規(guī)定一個(gè)最大深度.得到類圖的泛化深度后，可以判斷該深度是否超過該最大深度.

這里不給出以上定理的嚴(yán)格證明過程.后面將以一個(gè)具體的UML類圖形式化描述和檢測(cè)實(shí)例說明上述定理的有效性.

4 UML類圖形式化描述和檢測(cè)實(shí)例

下面給出一個(gè)基于二元關(guān)系和矩陣的UML類圖形式化描述和檢測(cè)實(shí)例.

圖2為一個(gè)在線學(xué)習(xí)系統(tǒng)[19]的UML類圖片段.設(shè)該UML類圖為G.

圖2 在線學(xué)習(xí)系統(tǒng)的UML類圖片段Fig.2 UML Class Diagram Fragment of an Online Learning System

4.1 答題系統(tǒng)類圖的形式化描述

記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可以表示為一個(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也可以用矩陣來形式化描述.下面的模型檢測(cè)過程將會(huì)用到屬性從屬關(guān)系矩陣MC-A、屬性類型矩陣MA-C、關(guān)聯(lián)關(guān)系矩陣MAss和泛化關(guān)系矩陣MGen，所以這里只給出這幾個(gè)矩陣.根據(jù)定義，可得：

4.2 答題系統(tǒng)類圖的檢測(cè)

這里給出檢測(cè)的原理，在后續(xù)的研究中將設(shè)計(jì)并實(shí)現(xiàn)UML類圖自動(dòng)檢測(cè)工具.

(1) 關(guān)聯(lián)關(guān)系的檢測(cè).

經(jīng)計(jì)算可知，

顯然MC-AMA-C≠M(fèi)Ass，由定理1可知類圖G存在關(guān)聯(lián)關(guān)系錯(cuò)誤.

而r12=1且s12=0，由定理1(1)可知類c1與類c2之間的關(guān)系定義錯(cuò)誤 (應(yīng)為關(guān)聯(lián)關(guān)系而非其他關(guān)系).

由圖2所示UML類圖可知，類Chapter包含類型為Exercise的屬性exercise，而類Chapter和類Exercise之間的關(guān)系卻錯(cuò)誤地定義為泛化關(guān)系.由此可見，定理1可以準(zhǔn)確地檢測(cè)出類圖中存在的關(guān)聯(lián)關(guān)系錯(cuò)誤.

(2) 遞歸泛化的檢測(cè).

由圖2所示UML類圖易見類Exercise、類Choice和類MultipleChoice之間的泛化關(guān)系為一個(gè)環(huán)狀，亦即模型存在遞歸泛化.

將類圖G進(jìn)行修改，去掉類Exercise繼承于類MultipleChoice的泛化關(guān)系，如圖3所示.設(shè)該類圖為G′.

圖3 修改后的UML模型Fig.3 Modified UML Class Diagram

此時(shí),

綜上所述，定理4可以有效地檢測(cè)出類圖中的遞歸泛化.

(3) 泛化深度的檢測(cè).

由圖3所示UML類圖易見泛化深度為2.由此可見，定理4可以準(zhǔn)確地檢測(cè)出類圖的泛化深度.

5 結(jié)論

UML模型的形式化描述和自動(dòng)檢測(cè)是當(dāng)前計(jì)算機(jī)領(lǐng)域的一個(gè)研究熱點(diǎn).本文提出的UML類圖形式化描述和檢測(cè)方法既具有完全形式化的圖形表示方法，又有堅(jiān)實(shí)的數(shù)學(xué)理論支撐.該方法借助了關(guān)系理論和矩陣?yán)碚?，可以進(jìn)一步開發(fā)自動(dòng)化工具對(duì)模型進(jìn)行嚴(yán)格地檢查和分析.本文提出的方法仍存在一些缺陷.下一步的研究工作將從以下幾個(gè)方面展開.

(1) 為了設(shè)計(jì)出高質(zhì)量的軟件，設(shè)計(jì)過程需要遵循一定的設(shè)計(jì)原則[20].如何根據(jù)這些原理對(duì)所設(shè)計(jì)的UML類圖進(jìn)行自動(dòng)優(yōu)化是下一步的研究重點(diǎn).

(2) 目前只得到UML類圖的形式化描述與檢測(cè)方法.在今后的研究中將對(duì)該方法進(jìn)行拓展，使其可以對(duì)UML的其他幾種圖進(jìn)行形式化描述和檢測(cè).

(3) 目前只得了幾種常見錯(cuò)誤的檢測(cè)定理.在今后的工作中將進(jìn)一步完善正確性檢測(cè)定理.

(4) 設(shè)計(jì)并實(shí)現(xiàn)UML類圖自動(dòng)檢測(cè)工具也是下一步研究的重點(diǎn).

[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活動(dòng)圖到Petri網(wǎng)的轉(zhuǎn)換方法及實(shí)現(xiàn)研究[J]. 計(jì)算機(jī)科學(xué), 2014, 41(7):143-147.

[6] 王 雷, 姜久雷, 王曉峰. 基于Petri網(wǎng)的設(shè)計(jì)模式形式化描述[J]. 計(jì)算機(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模型到可靠性分析模型的轉(zhuǎn)換方法[J]. 軟件學(xué)報(bào), 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].北京郵電大學(xué)學(xué)報(bào)，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-)，男，教授，博導(dǎo)，研究方向：軟件工程、并行計(jì)算，E-mail：wy8952@sohu.com

國家自然科學(xué)基金資助項(xiàng)目(60803159)，國家“973”計(jì)劃項(xiàng)目(2013CB228602))

TP312

A

1672-4321(2017)02-0109-06

*通訊作者 王 雷，研究方向：形式化開發(fā)方法、軟件體系結(jié)構(gòu)，E-mail: wanglei0823@foxmail.com