王博文 盛 楓 竇 亮 楊宗源

(華東師范大學(xué)信息科學(xué)技術(shù)學(xué)院 上海 200241)

UML類圖的形式規(guī)約與精化研究

王博文 盛 楓 竇 亮 楊宗源

(華東師范大學(xué)信息科學(xué)技術(shù)學(xué)院 上海 200241)

UML由于其廣泛的應(yīng)用和直觀的圖形化符號(hào)，成為了模型驅(qū)動(dòng)工程的重要組成部分。但UML本身缺乏精確的形式語(yǔ)義定義，缺少對(duì)其模型精化關(guān)系的形式化規(guī)范定義，對(duì)UML模型進(jìn)行形式驗(yàn)證變得尤為困難。UML類圖作為描述系統(tǒng)結(jié)構(gòu)的靜態(tài)模型，不具備完整的形式語(yǔ)義。從UML類圖的機(jī)械語(yǔ)義中抽取出形式規(guī)約，將UML類圖中的結(jié)構(gòu)和形式規(guī)約轉(zhuǎn)換成定理證明器Coq中的機(jī)械語(yǔ)義定義。此外，還提出了類圖的結(jié)構(gòu)精化操作，將模型間的精化關(guān)系在Coq中進(jìn)行形式化定義，并且對(duì)精化操作的原子操作進(jìn)行機(jī)械驗(yàn)證，保證其精化前后系統(tǒng)的結(jié)構(gòu)和語(yǔ)義保持一致。將UML和形式化方法相結(jié)合，為可驗(yàn)證的軟件設(shè)計(jì)精化框架提供了理論依據(jù)。

UML類圖 模型精化 Coq 機(jī)械語(yǔ)意

0 引 言

統(tǒng)一建模語(yǔ)言UML是一種通用的圖形化建模語(yǔ)言，具備直觀易懂特性，并且具有較好的可視化工具提供支持如Rational Rose、 Argo UML等，在模型驅(qū)動(dòng)工程中得到了廣泛的應(yīng)用，成為面向?qū)ο蠓治龊驮O(shè)計(jì)的工業(yè)標(biāo)準(zhǔn)。UML提供不同類型的圖，從不同方面和不同視角對(duì)系統(tǒng)進(jìn)行建模。然而，當(dāng)前的UML2.0使用半形式化的圖、約束和非形式化的自然語(yǔ)言文本進(jìn)行描述，缺乏精確的語(yǔ)義定義，會(huì)導(dǎo)致以下問題：(1)對(duì)模型理解的不一致性，即不同的人員對(duì)同一模型會(huì)有不同的理解；(2)難以實(shí)現(xiàn)迭代精化的開發(fā)過(guò)程；(3)難以對(duì)模型進(jìn)行分析以保證其正確性。

在之前的工作中[4]，我們使用定理證明器Coq[3]對(duì)UML序列圖和狀態(tài)圖的機(jī)械語(yǔ)義與精化操作進(jìn)行形式化描述和機(jī)械驗(yàn)證，并使用Kermeta[14]實(shí)現(xiàn)了序列圖和狀態(tài)圖的形式語(yǔ)義到Coq定義的自動(dòng)轉(zhuǎn)換。然而，由于序列圖和狀態(tài)圖是UML動(dòng)態(tài)圖，具有完整的指稱語(yǔ)義或操作語(yǔ)義，可在Coq中描述并實(shí)現(xiàn)機(jī)械驗(yàn)證。UML類圖作為描述系統(tǒng)結(jié)構(gòu)的靜態(tài)模型，不具備完整的形式語(yǔ)義，因此本文首先從UML類圖的形式語(yǔ)義中抽取出形式規(guī)約，即形式規(guī)約是UML類圖形式語(yǔ)義的具體體現(xiàn)。然后使用Coq對(duì)UML類圖的形式規(guī)約和結(jié)構(gòu)精化的原子操作進(jìn)行形式化描述與定義?；谏鲜龅男问矫枋觯瑢ML類圖的重要屬性與精化關(guān)系轉(zhuǎn)換為數(shù)學(xué)定理，在Coq中進(jìn)行形式化定義與驗(yàn)證。本文將半形式化的UML類圖與形式化方法相結(jié)合，彌補(bǔ)了半形式化UML的不足，通過(guò)對(duì)類圖及其精化操作的形式化描述與驗(yàn)證，保證UML模型及其精化的一致性和正確性，為可驗(yàn)證軟件設(shè)計(jì)模型精化框架提供了理論基礎(chǔ)。

1 定理證明器Coq

Coq是當(dāng)前被廣泛用于機(jī)械語(yǔ)義研究的交互式定理證明器，其內(nèi)置語(yǔ)言(Gallina)基于歸納構(gòu)造演算，且提供交互式的證明環(huán)境。歸納構(gòu)造演算是一種形式系統(tǒng)，結(jié)合了構(gòu)造邏輯和依賴類型的最新進(jìn)展。Coq中的歸納類型擴(kuò)展了傳統(tǒng)程序設(shè)計(jì)語(yǔ)言中有關(guān)類型定義的概念，融合遞歸類型和依賴積，具有更強(qiáng)的表達(dá)能力。與其他證明工具相比，Coq尤為適合對(duì)形式語(yǔ)法和語(yǔ)義進(jìn)行精確的表示。如Isabelle/HOL也可用于機(jī)械語(yǔ)義驗(yàn)證，但由于Isabelle/HOL[13]缺乏依賴類型，因此對(duì)一些正確性屬性的證明代碼量相對(duì)較多。Coq中常用的類型包括歸納類型和歸納謂詞。歸納類型適合對(duì)數(shù)據(jù)類型進(jìn)行建模，它可以表示無(wú)限集合，且每個(gè)元素都是在有限步驟內(nèi)構(gòu)造的。歸納謂詞可以對(duì)各種屬性進(jìn)行公式化，并可表示各種歸納數(shù)據(jù)類型之間的關(guān)系，適合描述系統(tǒng)之間的重要屬性。

Coq使用歸納類型來(lái)定義類型。例如，自然數(shù)的歸納類型可定義為：

Inductive nat ：Set :=

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

其中nat是歸納定義類型，屬于Set(類型的全域)中的值。類型nat包括兩個(gè)構(gòu)造子，第一個(gè)構(gòu)造子聲明O屬于自然數(shù)，第二個(gè)構(gòu)造子表示任意給定一個(gè)自然數(shù)n，S n仍然是個(gè)自然數(shù)，即任何自然數(shù)的后繼也是自然數(shù)。Coq還可以表示歸納定義的謂詞，表示數(shù)據(jù)類型的屬性或關(guān)系?；陬愋蚽at的定義，可以定義偶數(shù)的概念：

Inductive even : nat -> Prop :=

| O_even: even O

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

謂詞even的類型是nat->Prop，表示關(guān)于nat的命題。even n是n是偶數(shù)的一個(gè)證明。O_even表示 O 是偶數(shù)，Plus2_even表示對(duì)于任意的自然數(shù)n，如果n是偶數(shù)，則n+2也是偶數(shù)。關(guān)鍵字Definition用來(lái)定義新的數(shù)據(jù)類型，如Definition string_pair : Set := string * string定義了類型(string，string)。

2 類圖形式規(guī)約

UML的類圖是由多個(gè)類，類之間的關(guān)系以及這些關(guān)系的約束組成，是描述系統(tǒng)結(jié)構(gòu)的一種靜態(tài)模型，是構(gòu)建UML其他圖的基礎(chǔ)。類圖所包含的內(nèi)容有：類、關(guān)聯(lián)、關(guān)聯(lián)類和泛化等。本節(jié)將介紹UML類圖中各個(gè)元素的形式規(guī)約，并且在定理證明器Coq中形式化描述。

2.1 類

類是描述具有相同特征、約束和語(yǔ)義的一組對(duì)象的集合，是構(gòu)成類圖的基礎(chǔ)。在語(yǔ)法上，一個(gè)類是由類名、屬性和操作組成的，其中屬性由屬性名和屬性類型組成，操作由操作名和操作參數(shù)組成，每個(gè)操作參數(shù)具有參數(shù)名和參數(shù)類型。根據(jù)Evans[1]的UML類圖語(yǔ)法，本文定義ClassName和Name來(lái)表示類名與屬性、操作名集合：ClassName表示所有類的名字的集合，Name表示所有屬性、操作以及操作參數(shù)名的集合。使用ClassDec =(P，O，attrtype, opsigs)來(lái)形式定義類，其中P表示屬性的集合，O表示操作集合，attrtype函數(shù)將類中的屬性映射到屬性類型，具有Name -> Type類型，opsigs函數(shù)將類中的操作映射到相應(yīng)的操作參數(shù)，并且將參數(shù)映射到參數(shù)類型，具有Name -> (Name -> Type)類型。在Coq中，使用歸納類型定義包括類名(Class)，屬性(Property)，操作(Operation)和參數(shù)(Parameter_)等基本類型，關(guān)鍵字 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.

對(duì)于屬性、操作等類型，不同的類可能具有相同的屬性名或操作名，而對(duì)于類名來(lái)說(shuō)，不同類的類名必須是不同的。因此，UML類圖中的類可定義為類名Class到四元組ClassDec的歸納類型：

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

2.2 關(guān) 聯(lián)

在UML中，關(guān)聯(lián)關(guān)系表示類與類之間的關(guān)系，關(guān)聯(lián)可分為三類：一般關(guān)聯(lián)、聚合以及組合。聚合是一種特殊的關(guān)聯(lián)關(guān)系，表示類間的關(guān)系是整體和部分的關(guān)系。組合則是更強(qiáng)形式的關(guān)聯(lián)，整體有管理部分特有的職責(zé)并且具有一致的生命周期。在大部分情況下，類圖中的關(guān)聯(lián)指的是二元關(guān)聯(lián)，因此，本文僅僅考慮二元關(guān)聯(lián)。

在語(yǔ)法上，二元關(guān)聯(lián)用連接兩個(gè)類的實(shí)線表示，由關(guān)聯(lián)名和一對(duì)關(guān)聯(lián)端點(diǎn)(association end)組成。每個(gè)關(guān)聯(lián)端點(diǎn)具有角色名(role name)、多重性約束(multiplicity constraint)、附加類(attached class)和關(guān)聯(lián)類型(assockind)等元素。擴(kuò)展集合Name的定義域，使其包括所有可能的關(guān)聯(lián)名和角色名。關(guān)聯(lián)端點(diǎn)由四元組AssociationEnd = (rolename, multiplicity, attachedclass, aggregation)表示。UML類圖的多重性約束表示一個(gè)類與相關(guān)聯(lián)的類的單個(gè)實(shí)例可能相關(guān)的實(shí)例個(gè)數(shù)，即多重性約束了相關(guān)對(duì)象的數(shù)目。因此，本文使用自然數(shù)域(nat)來(lái)表示多重性的上界。附加類表示其與該關(guān)聯(lián)端點(diǎn)相連接的類，具有Class類型。aggregation表示關(guān)聯(lián)類型，具有一般關(guān)聯(lián)(none)，聚合(aggregate)和組合(composite)三種類型。在Coq中使用歸納類型Indutive來(lái)定義關(guān)聯(lián)類型：

Inductive assockind := none | aggregate | composite.

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

其中nat表示自然數(shù)集合。對(duì)于關(guān)聯(lián)關(guān)系來(lái)說(shuō)，具有以下約束條件：

定義1 對(duì)于一組關(guān)聯(lián)關(guān)系(n, (e1,e2))，關(guān)聯(lián)名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函數(shù)是Coq內(nèi)置函數(shù)，用于判定某個(gè)元素是否屬于某個(gè)集合。

定義2 對(duì)于聚類關(guān)系，兩個(gè)關(guān)聯(lián)端點(diǎn)的關(guān)聯(lián)類型分別為aggregate和none；對(duì)于組合關(guān)系，兩個(gè)關(guān)聯(lián)端點(diǎn)的關(guān)聯(lián)類型分別為composite和none；對(duì)于組合關(guān)系，關(guān)聯(lián)端點(diǎn)的關(guān)聯(lián)類型為composite的端點(diǎn)，其多重性約束的值為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).

函數(shù)or表示Coq內(nèi)置的邏輯或操作。

定義3 對(duì)于所有的關(guān)聯(lián)關(guān)系，其關(guān)聯(lián)名必須是唯一的，即如果 (n1,(e1,e2))和(n2,(e3,e4))均屬于集合associations，e1 ≠ e3，e2 ≠ e4，e1對(duì)應(yīng)的附加類與e3相同且e2對(duì)應(yīng)的附加類與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.

如果類圖中的關(guān)聯(lián)關(guān)系符合上述語(yǔ)法和約束，則認(rèn)為其符合UML類圖的形式規(guī)范。使用Coq中的子集類型來(lái)表示符合上述約束的數(shù)據(jù)類型，即將數(shù)據(jù)類型和該類型上的約束謂詞相結(jié)合，從而得到滿足該謂詞的數(shù)據(jù)類型：

Definition umlassociations :=

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

2.3 關(guān)聯(lián)類

關(guān)聯(lián)類是一個(gè)擁有關(guān)聯(lián)關(guān)系和類特性的模型元素。一個(gè)關(guān)聯(lián)類可以看作是一組擁有類特性的關(guān)聯(lián)關(guān)系，或者是一個(gè)擁有關(guān)聯(lián)特性的類。它不僅僅用于連接一些分類器(classifier)，還定義了屬于關(guān)聯(lián)關(guān)系本身的特征，這些特征是只屬于關(guān)聯(lián)關(guān)系本身而不屬于任何關(guān)聯(lián)分類器的。關(guān)聯(lián)類由類和一對(duì)關(guān)聯(lián)端點(diǎn)組成，由二元組AssocClassDec = (assoc, (assoEnd1, assoEnd2))表示，其中assoc表示類，是集合umlclass的元素，assoEnd1和assoEnd2是類型AssociationEnd的關(guān)聯(lián)端點(diǎn)：

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

對(duì)于關(guān)聯(lián)類來(lái)說(shuō)，具有以下約束條件：

定義4 對(duì)于任意關(guān)聯(lián)類(umlclass,(e1,e2))，e1.rolename ≠ e2.roolename，并且關(guān)聯(lián)類型的值必須是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.

其中函數(shù)asslink1和asslink2表示關(guān)聯(lián)類中的一組關(guān)聯(lián)端點(diǎn)，函數(shù)rolename表示關(guān)聯(lián)端點(diǎn)中的角色名。

定義5 對(duì)于任意關(guān)聯(lián)類(umlclass,(e1,e2))，附加類中的角色名不屬于關(guān)聯(lián)類中類的屬性名集合。

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)).

其中函數(shù)class_pro返回類u中的屬性集合，函數(shù)makeattr_name將屬性集合中的元素類型由Property轉(zhuǎn)換為string類型。

定義6 對(duì)于任意關(guān)聯(lián)類(umlclass,(e1,e2))，關(guān)聯(lián)端點(diǎn)中的附加類不是關(guān)聯(lián)類中的類，即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.

其中函數(shù)class_eq判定兩個(gè)類型為Class的元素是否相等。

UML類圖的關(guān)聯(lián)類的形式化表示是滿足上述約束的類型為AssocClassDec的數(shù)據(jù)類型：

Definition UMLAssocClass :=

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

2.4 泛 化

泛化關(guān)系是父類與子類之間的關(guān)系，子類繼承父類的屬性和操作，并且添加新的屬性和操作，或者修改父類的某些操作[2]，是實(shí)現(xiàn)多態(tài)的基礎(chǔ)。本文使用集合superclasses和subclasses表示泛化關(guān)系中的父類和子類。superclasses表示類名Class中的父類的有限集合，subclasseses表示類名Class的每個(gè)父類的子類集合的集合。使用二元組(class, subclasees)表示一組泛化關(guān)系，其中class表示父類，subclasses表示該父類下的子類集合，列表類型list來(lái)定義泛化關(guān)系的集合：

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函數(shù)返回多元組中的第一個(gè)元素，snd函數(shù)是返回多元組中的第二個(gè)元素，subclasses函數(shù)是對(duì)于給定的父類，從泛化關(guān)系集合中返回其對(duì)應(yīng)的子類集合; superclasses函數(shù)的功能是返回泛化關(guān)系集合中的所有父類集合，中綴::表示連接一個(gè)元素(fst x)與集合(superclasses A)，將元素置入列表的首位。

對(duì)于泛化關(guān)系而言，具有以下約束：

定義7 對(duì)于任意泛化關(guān)系，父類與子類均不具備自反繼承性(reflexive inheritance)，即每一個(gè)類不可能是該類的父類，也不是該類的子類，父類集合與子類集合不相交。

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類圖中的泛化關(guān)系的形式化表示是滿足上述約束的類型為GenDec的數(shù)據(jù)類型：

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

2.5 類 圖

UML類圖是包括類、關(guān)聯(lián)類、關(guān)聯(lián)關(guān)系和泛化關(guān)系等類型的集合，由四元組UMLClassDiagram= (UMLClass, UMLAssociation, UMLAssocClass, UMLGeneralizetion)表示：

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

對(duì)于類圖而言，具有以下約束：

定義8 類圖中的UMLClass集合的類名集合與關(guān)聯(lián)類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)).

其中函數(shù)uml_assocclass從類圖中取出關(guān)聯(lián)類UMLAssocClass的集合，函數(shù)assoc_classname返回關(guān)聯(lián)類UMLAssocClass中的類名集合，函數(shù)makeclass_name返回UMLClass集合中的類名集合。

定義9 類圖中的關(guān)聯(lián)關(guān)系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)).

其中函數(shù)assoc_attachclasses計(jì)算類圖中的關(guān)聯(lián)類的類名集合，函數(shù)uml_assoc返回類圖中的關(guān)聯(lián)關(guān)系集合，函數(shù)uml_class返回類圖中的類的類名集合。

定義10 類圖的泛化關(guān)系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)).

函數(shù)allclasses計(jì)算泛化關(guān)系中的父類名和子類名的集合，函數(shù)uml_gen返回類圖中的泛化關(guān)系的集合。

UML類圖的形式化定義是滿足上述約束的類型為UMLClassDiagram的數(shù)據(jù)類型：

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

3 精化操作

類圖是由所有類、類之間的關(guān)系和關(guān)系的約束組成的集合，主要體現(xiàn)了需求工程中系統(tǒng)的靜態(tài)結(jié)構(gòu)。對(duì)于類圖的精化操作研究，本文主要側(cè)重于系統(tǒng)結(jié)構(gòu)方面的精化操作，即添加、刪除或修改類、關(guān)聯(lián)類、關(guān)聯(lián)關(guān)系以及泛化關(guān)系。類圖的精化操作往往是一種迭代過(guò)程：給出一個(gè)抽象的類圖模型，通過(guò)一系列復(fù)雜的精化操作，最終得到一個(gè)具體的類圖模型。每個(gè)中間模型都必須與其精化后的模型保持一致，即精化前后系統(tǒng)的結(jié)構(gòu)和語(yǔ)義保持一致。本節(jié)給出四種類圖精化的原子操作，復(fù)雜的精化操作可通過(guò)有限次的調(diào)用原子操作實(shí)現(xiàn):

3.1 添 加

向已有的類圖中添加新的類或關(guān)聯(lián)類，函數(shù)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 刪 除

從已有的類圖中刪除指定的類或關(guān)聯(lián)類，分為以下兩種情況：

1) 如果刪除的對(duì)象是關(guān)聯(lián)類c，那么直接刪除集合UMLAssocClass中的關(guān)聯(lián)類名為c的元素，包括其關(guān)聯(lián)類和關(guān)聯(lián)端點(diǎn)；

2) 如果刪除的對(duì)象是集合UMLClass中的一般類，首先搜索關(guān)聯(lián)關(guān)系集合、關(guān)聯(lián)類集合和泛化關(guān)系集合，如果關(guān)聯(lián)端點(diǎn)或泛化關(guān)系中存在該類名，那么先執(zhí)行拆分操作，刪除其關(guān)聯(lián)關(guān)系或泛化關(guān)系。然后調(diào)用函數(shù)re_class，通過(guò)搜索集合umlclass中是否存在c，如果存在則將其從umlclass中刪除。函數(shù)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 鏈 接

向已有的類圖中添加新的關(guān)聯(lián)關(guān)系或泛化關(guān)系，其Coq定義與添加操作類似。

3.4 拆 分

從已有的類圖中刪除指定的關(guān)聯(lián)關(guān)系或泛化關(guān)系，其Coq定義與刪除操作類似。

定理1 設(shè)u:umlclass, UCD:UMLClassDiagram，如果u不屬于集合ClassName并且UCD滿足上述類圖的形式規(guī)約UML_post UCD，那么執(zhí)行添加操作后得到的類圖也滿足形式規(guī)約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 設(shè)a:associations, UCD:UMLClassDiagram,如果a不屬于類圖UCD的關(guān)聯(lián)關(guān)系，并且UCD中的所有關(guān)聯(lián)關(guān)系a均符合上述形式規(guī)約，那么執(zhí)行鏈接操作后得到的類圖也滿足形式規(guī)約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).

其中函數(shù)uml_assoc是返回類圖UMLClassDiagram中的關(guān)聯(lián)關(guān)系的集合。

上述定理表明：如果類圖滿足上述的形式規(guī)約，那么它執(zhí)行上述四種精化操作后得到的類圖也滿足上述形式規(guī)約。復(fù)雜的類圖精化操作可以通過(guò)有限次的原子精化操作得到，如添加一個(gè)類，首先在UMLClass集合中添加該類的具體信息，然后在執(zhí)行鏈接操作將其與該類圖中的其他類相關(guān)聯(lián)。對(duì)精化操作的原子操作的機(jī)械驗(yàn)證，保證了其復(fù)雜的精化操作的正確性，從而驗(yàn)證了UML類圖精化操作前后的結(jié)構(gòu)和語(yǔ)義的一致性。

4 實(shí)例驗(yàn)證

本節(jié)給出一個(gè)圖書館系統(tǒng)的類圖，如圖1所示，我們將其轉(zhuǎn)換成上述由定理證明器Coq所描述的形式規(guī)約，并且驗(yàn)證該類圖符合UML類圖的形式化規(guī)約。圖1包括三個(gè)實(shí)體類Reader，Copy和Publication。類Publication可以泛化成兩個(gè)子類Periodical和Book。關(guān)聯(lián)類Loan表示類Reader和類Copy之間的關(guān)系，并且具有類Loan。關(guān)聯(lián)關(guān)系catalogue將類Copy和類Publication相關(guān)聯(lián)。

根據(jù)上述的定義，由于篇幅有限，本文只給出上述類圖的部分形式化規(guī)約定義：

首先，定義各個(gè)類的名字，其類型為Class如class “Loan”表示類名為L(zhǎng)oan的類，其次定義每個(gè)類的屬性與操作集合如property “l(fā)oaddate”表示屬性loaddate，operation “CheckOverdue”表示操作CheckOverdue，類的屬性的類型為Property，Loanproperty和Loanoperation分別是類圖Loan的屬性和操作的集合，LoanClass是將類名Loan到其具體參數(shù)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類圖的實(shí)例

接著，定義類圖的關(guān)聯(lián)關(guān)系：圖1中類Copy與Publication具有關(guān)聯(lián)關(guān)系，asscollection表示與類Copy相連接的關(guān)聯(lián)端點(diǎn)，角色名為collection，多重性是0...*，由于Coq的自然數(shù)域只是表示有限的數(shù)，因此設(shè)多重性的最大值為100，附加類是Copy，關(guān)聯(lián)類型為none。coll2detail表示上述關(guān)聯(lián)關(guān)系，其關(guān)聯(lián)名為catalogue，關(guān)聯(lián)端點(diǎn)為asscollection和assdetail。關(guān)聯(lián)類與泛化關(guān)系與上述類似，不再贅述。

(* 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)

為了說(shuō)明上述類圖是符合類圖的形式規(guī)約，本文通過(guò)驗(yàn)證上述形式化定義滿足形式規(guī)約命題，由于篇幅有限，只給出定義7的Coq證明過(guò)程：

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 相關(guān)工作

將UML和形式化方法相結(jié)合是國(guó)內(nèi)外廣大學(xué)者和科研組織的一個(gè)研究熱點(diǎn)，目的是彌補(bǔ)半形式化的UML缺乏精確語(yǔ)義定義的不足。目前UML形式化方法有兩種思路：一是對(duì)UML核心語(yǔ)法進(jìn)行形式化，使得UML成為符合形式化規(guī)范的語(yǔ)言，如英國(guó)PUML 工作組在元模型層次(UMLMeta-model)對(duì)UML進(jìn)行形式化，保證在此基礎(chǔ)上建立的UML 模型層和用戶對(duì)象層有可靠的數(shù)學(xué)模型基礎(chǔ)，可對(duì)構(gòu)造、操縱和精化模型提供一種通用的方法。另一種是轉(zhuǎn)換法，利用形式化語(yǔ)言在不丟失或者少丟失信息的前提下對(duì)UML進(jìn)行形式化，如Kim等[5-6]將UML類圖轉(zhuǎn)換為Z形式規(guī)格說(shuō)明，然而Kim僅考慮類、類屬性、類操作、關(guān)聯(lián)以及泛化的轉(zhuǎn)換，沒有考慮模型中的約束條件。

Tanuan[7]、Lano[8]基于Meyer等[9]的部分工作，提出了從UML結(jié)構(gòu)概念到B形式規(guī)約的派生方案，將每個(gè)類屬性、關(guān)聯(lián)和狀態(tài)模型轉(zhuǎn)換成B變量，類之間的關(guān)系形式化為代表類的變量的謂詞不變式。Cali[10]使用描述邏輯(Description Logics)對(duì)UML類圖進(jìn)行形式化描述。Szlenk[11]定義了類圖的形式語(yǔ)義，并且介紹了類圖中的一致性問題。Anastasakis[12]將帶OCL約束的UML自動(dòng)轉(zhuǎn)換到Alloy代碼。黃春榮等[15]給出了UML模型到COOZ規(guī)約的一種系統(tǒng)轉(zhuǎn)換方法，用COOZ類形式化描述類圖中的元素語(yǔ)法和語(yǔ)義。楊敬中等[16]提出了用XYZ/E來(lái)描述UML類圖的形式化語(yǔ)言，XYZ/E是一種面向軟件開發(fā)全過(guò)程的時(shí)序邏輯語(yǔ)言，既能表示軟件系統(tǒng)的規(guī)范與性質(zhì)，又能表示軟件系統(tǒng)的數(shù)學(xué)模型與程序?qū)崿F(xiàn)。

6 結(jié) 語(yǔ)

本文從類圖的形式語(yǔ)義中抽取出形式規(guī)約，使用定理證明器Coq描述UML類圖的形式規(guī)約，提出了UML類圖的結(jié)構(gòu)精化操作，并且在Coq中對(duì)其進(jìn)行形式化描述?；谏鲜龅男问揭?guī)約，UML類圖和精化操作的重要屬性轉(zhuǎn)換為數(shù)學(xué)定理，在Coq中形式描述并機(jī)械驗(yàn)證。此外，本文通過(guò)一個(gè)小型的類圖實(shí)例表明了上述形式規(guī)約的可行性與正確性。與之前的UML序列圖和狀態(tài)圖的機(jī)械驗(yàn)證相結(jié)合，為提出可驗(yàn)證的軟件設(shè)計(jì)模型精化框架提供理論基礎(chǔ)。

基于現(xiàn)有工作，我們將從以下方面做進(jìn)一步研究：(1)添加UML類圖的OCL約束的形式化定義，使得帶OCL約束的UML類圖能夠形式化描述；(2)使用Kermeta轉(zhuǎn)換工具，實(shí)現(xiàn)從UML類圖轉(zhuǎn)換到Coq定義的形式化描述的自動(dòng)化轉(zhuǎn)換工具；(3)實(shí)現(xiàn)包括類圖、序列圖和狀態(tài)圖的可驗(yàn)證軟件設(shè)計(jì)模型精化框架。

[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] 黃春榮,李宣東,鄭國(guó)梁.UML模型到COOZ規(guī)約的形式化轉(zhuǎn)換[J].計(jì)算機(jī)工程與應(yīng)用,2003,39(20):89-91.

[16] 楊敬中,張廣泉,戎玫.UML2.0類圖的一種形式化描述方法[J].計(jì)算機(jī)科學(xué),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。國(guó)家自然科學(xué)基金項(xiàng)目(61070226)。王博文，碩士生，主研領(lǐng)域：UML和軟件形式化驗(yàn)證。盛楓，博士生。竇亮，講師。楊宗源，教授。

TP301.2

A

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