ＵＭＬ類圖靜態模型的形式化

摘 要： B方法主要是用抽象機來描述軟件系統的規范說明，且有大量工具支持。UML作為新一代面向對象建模語言得到了廣泛的支持，已經成為事實上的工業標準。UML 圖形是模型元素集合的可視化表示，類圖表達了面向對象系統分析中的最基本元素——類和類之間聯系，而類之間的依賴關系是類之間聯系中的最重要、最普遍的一種聯系。本文旨之討論如何讓用B方法來描述UML類圖，從而能提高軟件開發的效率、降低成本，也能改善軟件工程的質量。

關鍵詞： UML類圖 B方法 靜態模型 形式化

統一建模語言UML作為新一代面向對象建模語言得到了廣泛的支持，已經成為事實上的工業標準。UML不僅支持面向對象分析與設計，而且支持從需求分析開始的軟件開發的全過程，已大范圍地用于現代企業集成信息系統的設計和開發當中。UML圖形是模型元素集合的可視化表示。UML定義了9種圖形，其中類圖表達了面向對象系統分析中的最基本元素——類和類之間聯系，而類之間的依賴關系是類之間聯系中的最重要、最普遍的一種聯系。

1.UML類圖簡介

UML類圖表達的是對象模型的靜態結構。其中一部分圖形元素是基本的，如類、關聯等，對于任何面向對象模型都是必不可少的。

類圖表達一組類和它們的聯系，在類圖中，一方面描述各個類本身的組成，即類的屬性、操作和對對象的約束，另一方面描述系統中類之間的靜態的聯系，其主要靜態聯系類型有關聯、聚集、泛化、依賴等。

面向對象系統設計一般運用都是規模較大的空間，類的數目眾多、類之間的關系錯綜復雜，設計者很難直接從類圖中理清類與類之間的依賴關系。然而，面向對象系統基于UML語言在分析和設計過程中，已經生成了許多類圖，如果能合理、有效地利用這些已經生成的成果，不僅能提高軟件開發的效率、降低成本，而且能改善軟件工程的質量。

2.B語言

B語言屬于基于模型的規格說明符號語言的范疇，是一種基于對象的形式化語言。它以規格說明語言Z語言的研究為背景，在引入一些面向對象機制等特點的同時，保留了Z語言的優點［５］。B語言使用相對簡單，且人們熟悉的符號表示法(廣義代換)來表達狀態的轉換，從軟件的規格說明到編碼的形成是一致的形式描述，使程序和程序的規則說明處于統一的數學框架之下，以一種基于集合論的符號表示法來書寫，減少了出現語義錯誤的可能性。這種數學框架是通過謂詞變換和擴展的Dijkstra最弱前置條件提供的［１］。B語言的抽象機非常類似于Effiel中的類的概念，或者Ada語言的包。

3.UML類圖靜態模型的形式化

UML類圖模型由對象類的命名方框構成，方框中列出了類的所有屬性及其操作，實體之間的關系用連線表示。一般說來，UML類圖中的類將表示為B機器，它封裝了可能的和存在的該類類型的屬性集合，以及對這些屬性的操作集合。類之間的關聯關系使用B機器的包含INCLUDES機制表示，繼承關系可以使用EXTENDS結構化機制來表示。

下面我們給出把UML類圖模型映射到B機器系統的基本方法和過程：

（1）標識類圖中的實體類型族，也就是實體類型集合，這些實體類型是一個給定類型T的子類型，而T本身沒有父類型。

（2）標識每個族內類型的操作和屬性所需要的訪問路徑，這些訪問是針對其它族中的類型。

（3）產生一個有向無環圖，圖中的節點就是類型族，圖中的邊是節點之間的包含關系USES或SEES。

（4）按照下面給出的步驟，為每個類型族定義機器，并使用上一步標識的關系包含其它的機器［６］。

根據上述方法，一個類圖的轉換可以寫成如下形式：（假設類名為實體類Entity，ENTITY為一實體集合，T1——Tn都是T類型的子類型）

MACHINE Entity

SETS

ENTITY

VARIABLES

Entities，

Att1，att2，...，attn

INVARIANT

entitues?哿ENTITY att1∈entites→T1 att2∈entites→T2... attn∈entites→Tn

...

END［３］

該機器是一組Entity實例的模型，而不是一個單獨的實體。集合ENTITY代表Entity實例的所有可能同類體的集合，entities代表當前已有的Entity實例的對象同類體集合。Entity實例的標準創建操作為：

i ←create_entity(att1_val，...，attn_val)=

PRE att1_val∈T1 ...attn_val∈Tn entities ENTITY

THEN

ANY j

WHERE

j∈ENTITY- entities

THEN

I：=j‖

entities：= entities∪{j}‖

att1(j)：=att1_val‖

...

attn (j)：=attn_val

END

END［４］

如果類模型的實體之間存在某些關系，那么T1，T2，...，Tn中的某些將涉及其它的實體，比如Entity2，Entity3，...，這時，我們要查看SEE或者使用USE相關的機器：

MACHINE Entity

SEES Entity2，Entity3，...

...

END

如果在Entity的不變式中只需使用同類體集合ENTITY2，ENTITY3，...，那么我們可以使用SEES。如果需要更具體的并且要使用已有的實體集entity2等作為不變式中的范圍類型，那么要使用USES。

我們還可以使用一個參數對一個將允許的給定實體的最大實例數給出限制：

MACHINE Entity (maxEntity)

CONSTRAINTS

maxEntity≥1

...

PROPERTIES

Card (ENTITY)=maxEntity

INVARIANT

Entities?哿ENTITY ...

END

如果Entity2繼承Entity1，那么需要把約束entities2 ( entities1放在標識超類的機器不變式中。

MACHINE Entity1

SETS

ENTITY1

VARIABLES

entities1，entities2

INVARIANT

entities1?哿ENTITY1(

entities2 ?哿entities1

...

END［２］

4.結語

本文討論如何讓用B方法來描述UML類圖，從而為提高軟件開發的效率、降低成本打下了基礎，并能大大地改善軟件工程的質量。

參考文獻：

［1］裘宗燕譯.Ｂ方法.電子工業出版社，2004，06.

［2］Kevin Lano.The B Language and Method：A Guide to Practice Formal Development.Springer Verlag，1996.

［3］B-Core Ltd.B-toolkit User’s Manual.Oxford（UK），1996.

［4］Emil Sekerinski and Rafik Zurob.Translation Statecharts to B.Spinger-Verlag，McMaster University，2003.

［5］鄒盛榮，鄭國梁.B語言和方法與Z、VDM的比較.計算機科學，2002（10）：136-138.

［6］鄒盛榮，鄭國梁.形式化方法B和UML的結合研究.中國科技論文在線，2003中國計算機大會.