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

王博文 盛 楓 竇 亮 楊宗源

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

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

王博文 盛 楓 竇 亮 楊宗源

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

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

UML類圖 模型精化 Coq 機械語意

0 引 言

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

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

1 定理證明器Coq

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

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

Inductive nat ：Set :=

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

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

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是偶數(shù)的一個證明。O_even表示 O 是偶數(shù)，Plus2_even表示對于任意的自然數(shù)n，如果n是偶數(shù)，則n+2也是偶數(shù)。關鍵字Definition用來定義新的數(shù)據(jù)類型，如Definition string_pair : Set := string * string定義了類型(string，string)。

2 類圖形式規(guī)約

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

2.1 類

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

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

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

Inductive assockind := none | aggregate | composite.

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

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

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

定義2 對于聚類關系，兩個關聯(lián)端點的關聯(lián)類型分別為aggregate和none；對于組合關系，兩個關聯(lián)端點的關聯(lián)類型分別為composite和none；對于組合關系，關聯(lián)端點的關聯(lián)類型為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).

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

定義3 對于所有的關聯(lián)關系，其關聯(lián)名必須是唯一的，即如果 (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.

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

Definition umlassociations :=

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

2.3 關聯(lián)類

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

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

對于關聯(lián)類來說，具有以下約束條件：

定義4 對于任意關聯(lián)類(umlclass,(e1,e2))，e1.rolename ≠ e2.roolename，并且關聯(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表示關聯(lián)類中的一組關聯(lián)端點，函數(shù)rolename表示關聯(lián)端點中的角色名。

定義5 對于任意關聯(lián)類(umlclass,(e1,e2))，附加類中的角色名不屬于關聯(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轉換為string類型。

定義6 對于任意關聯(lián)類(umlclass,(e1,e2))，關聯(liá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判定兩個類型為Class的元素是否相等。

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

Definition UMLAssocClass :=

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

2.4 泛 化

泛化關系是父類與子類之間的關系，子類繼承父類的屬性和操作，并且添加新的屬性和操作，或者修改父類的某些操作[2]，是實現(xiàn)多態(tài)的基礎。本文使用集合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函數(shù)返回多元組中的第一個元素，snd函數(shù)是返回多元組中的第二個元素，subclasses函數(shù)是對于給定的父類，從泛化關系集合中返回其對應的子類集合; superclasses函數(shù)的功能是返回泛化關系集合中的所有父類集合，中綴::表示連接一個元素(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的數(shù)據(jù)類型：

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

2.5 類 圖

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

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

對于類圖而言，具有以下約束：

定義8 類圖中的UMLClass集合的類名集合與關聯(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從類圖中取出關聯(lián)類UMLAssocClass的集合，函數(shù)assoc_classname返回關聯(lián)類UMLAssocClass中的類名集合，函數(shù)makeclass_name返回UMLClass集合中的類名集合。

定義9 類圖中的關聯(liá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計算類圖中的關聯(lián)類的類名集合，函數(shù)uml_assoc返回類圖中的關聯(lián)關系集合，函數(shù)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)).

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

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

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

3 精化操作

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

3.1 添 加

向已有的類圖中添加新的類或關聯(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 刪 除

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

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

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

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

3.4 拆 分

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

定理1 設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 設a:associations, UCD:UMLClassDiagram,如果a不屬于類圖UCD的關聯(lián)關系，并且UCD中的所有關聯(liá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中的關聯(lián)關系的集合。

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

4 實例驗證

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

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

首先，定義各個類的名字，其類型為Class如class “Loan”表示類名為Loan的類，其次定義每個類的屬性與操作集合如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類圖的實例

接著，定義類圖的關聯(lián)關系：圖1中類Copy與Publication具有關聯(lián)關系，asscollection表示與類Copy相連接的關聯(lián)端點，角色名為collection，多重性是0...*，由于Coq的自然數(shù)域只是表示有限的數(shù)，因此設多重性的最大值為100，附加類是Copy，關聯(lián)類型為none。coll2detail表示上述關聯(lián)關系，其關聯(lián)名為catalogue，關聯(lián)端點為asscollection和assdetail。關聯(liá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)

為了說明上述類圖是符合類圖的形式規(guī)約，本文通過驗證上述形式化定義滿足形式規(guī)約命題，由于篇幅有限，只給出定義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成為符合形式化規(guī)范的語言，如英國PUML 工作組在元模型層次(UMLMeta-model)對UML進行形式化，保證在此基礎上建立的UML 模型層和用戶對象層有可靠的數(shù)學模型基礎，可對構造、操縱和精化模型提供一種通用的方法。另一種是轉換法，利用形式化語言在不丟失或者少丟失信息的前提下對UML進行形式化，如Kim等[5-6]將UML類圖轉換為Z形式規(guī)格說明，然而Kim僅考慮類、類屬性、類操作、關聯(lián)以及泛化的轉換，沒有考慮模型中的約束條件。

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

6 結 語

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

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

[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規(guī)約的形式化轉換[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