ＵＭＬ類(lèi)圖靜態(tài)模型的形式化

摘 要： B方法主要是用抽象機(jī)來(lái)描述軟件系統(tǒng)的規(guī)范說(shuō)明，且有大量工具支持。UML作為新一代面向?qū)ο蠼ＵZ(yǔ)言得到了廣泛的支持，已經(jīng)成為事實(shí)上的工業(yè)標(biāo)準(zhǔn)。UML 圖形是模型元素集合的可視化表示，類(lèi)圖表達(dá)了面向?qū)ο笙到y(tǒng)分析中的最基本元素——類(lèi)和類(lèi)之間聯(lián)系，而類(lèi)之間的依賴關(guān)系是類(lèi)之間聯(lián)系中的最重要、最普遍的一種聯(lián)系。本文旨之討論如何讓用B方法來(lái)描述UML類(lèi)圖，從而能提高軟件開(kāi)發(fā)的效率、降低成本，也能改善軟件工程的質(zhì)量。

關(guān)鍵詞： UML類(lèi)圖 B方法 靜態(tài)模型 形式化

統(tǒng)一建模語(yǔ)言UML作為新一代面向?qū)ο蠼ＵZ(yǔ)言得到了廣泛的支持，已經(jīng)成為事實(shí)上的工業(yè)標(biāo)準(zhǔn)。UML不僅支持面向?qū)ο蠓治雠c設(shè)計(jì)，而且支持從需求分析開(kāi)始的軟件開(kāi)發(fā)的全過(guò)程，已大范圍地用于現(xiàn)代企業(yè)集成信息系統(tǒng)的設(shè)計(jì)和開(kāi)發(fā)當(dāng)中。UML圖形是模型元素集合的可視化表示。UML定義了9種圖形，其中類(lèi)圖表達(dá)了面向?qū)ο笙到y(tǒng)分析中的最基本元素——類(lèi)和類(lèi)之間聯(lián)系，而類(lèi)之間的依賴關(guān)系是類(lèi)之間聯(lián)系中的最重要、最普遍的一種聯(lián)系。

1.UML類(lèi)圖簡(jiǎn)介

UML類(lèi)圖表達(dá)的是對(duì)象模型的靜態(tài)結(jié)構(gòu)。其中一部分圖形元素是基本的，如類(lèi)、關(guān)聯(lián)等，對(duì)于任何面向?qū)ο竽Ｐ投际潜夭豢缮俚摹?/p>

類(lèi)圖表達(dá)一組類(lèi)和它們的聯(lián)系，在類(lèi)圖中，一方面描述各個(gè)類(lèi)本身的組成，即類(lèi)的屬性、操作和對(duì)對(duì)象的約束，另一方面描述系統(tǒng)中類(lèi)之間的靜態(tài)的聯(lián)系，其主要靜態(tài)聯(lián)系類(lèi)型有關(guān)聯(lián)、聚集、泛化、依賴等。

面向?qū)ο笙到y(tǒng)設(shè)計(jì)一般運(yùn)用都是規(guī)模較大的空間，類(lèi)的數(shù)目眾多、類(lèi)之間的關(guān)系錯(cuò)綜復(fù)雜，設(shè)計(jì)者很難直接從類(lèi)圖中理清類(lèi)與類(lèi)之間的依賴關(guān)系。然而，面向?qū)ο笙到y(tǒng)基于UML語(yǔ)言在分析和設(shè)計(jì)過(guò)程中，已經(jīng)生成了許多類(lèi)圖，如果能合理、有效地利用這些已經(jīng)生成的成果，不僅能提高軟件開(kāi)發(fā)的效率、降低成本，而且能改善軟件工程的質(zhì)量。

2.B語(yǔ)言

B語(yǔ)言屬于基于模型的規(guī)格說(shuō)明符號(hào)語(yǔ)言的范疇，是一種基于對(duì)象的形式化語(yǔ)言。它以規(guī)格說(shuō)明語(yǔ)言Z語(yǔ)言的研究為背景，在引入一些面向?qū)ο髾C(jī)制等特點(diǎn)的同時(shí)，保留了Z語(yǔ)言的優(yōu)點(diǎn)［５］。B語(yǔ)言使用相對(duì)簡(jiǎn)單，且人們熟悉的符號(hào)表示法(廣義代換)來(lái)表達(dá)狀態(tài)的轉(zhuǎn)換，從軟件的規(guī)格說(shuō)明到編碼的形成是一致的形式描述，使程序和程序的規(guī)則說(shuō)明處于統(tǒng)一的數(shù)學(xué)框架之下，以一種基于集合論的符號(hào)表示法來(lái)書(shū)寫(xiě)，減少了出現(xiàn)語(yǔ)義錯(cuò)誤的可能性。這種數(shù)學(xué)框架是通過(guò)謂詞變換和擴(kuò)展的Dijkstra最弱前置條件提供的［１］。B語(yǔ)言的抽象機(jī)非常類(lèi)似于Effiel中的類(lèi)的概念，或者Ada語(yǔ)言的包。

3.UML類(lèi)圖靜態(tài)模型的形式化

UML類(lèi)圖模型由對(duì)象類(lèi)的命名方框構(gòu)成，方框中列出了類(lèi)的所有屬性及其操作，實(shí)體之間的關(guān)系用連線表示。一般說(shuō)來(lái)，UML類(lèi)圖中的類(lèi)將表示為B機(jī)器，它封裝了可能的和存在的該類(lèi)類(lèi)型的屬性集合，以及對(duì)這些屬性的操作集合。類(lèi)之間的關(guān)聯(lián)關(guān)系使用B機(jī)器的包含INCLUDES機(jī)制表示，繼承關(guān)系可以使用EXTENDS結(jié)構(gòu)化機(jī)制來(lái)表示。

下面我們給出把UML類(lèi)圖模型映射到B機(jī)器系統(tǒng)的基本方法和過(guò)程：

（1）標(biāo)識(shí)類(lèi)圖中的實(shí)體類(lèi)型族，也就是實(shí)體類(lèi)型集合，這些實(shí)體類(lèi)型是一個(gè)給定類(lèi)型T的子類(lèi)型，而T本身沒(méi)有父類(lèi)型。

（2）標(biāo)識(shí)每個(gè)族內(nèi)類(lèi)型的操作和屬性所需要的訪問(wèn)路徑，這些訪問(wèn)是針對(duì)其它族中的類(lèi)型。

（3）產(chǎn)生一個(gè)有向無(wú)環(huán)圖，圖中的節(jié)點(diǎn)就是類(lèi)型族，圖中的邊是節(jié)點(diǎn)之間的包含關(guān)系USES或SEES。

（4）按照下面給出的步驟，為每個(gè)類(lèi)型族定義機(jī)器，并使用上一步標(biāo)識(shí)的關(guān)系包含其它的機(jī)器［６］。

根據(jù)上述方法，一個(gè)類(lèi)圖的轉(zhuǎn)換可以寫(xiě)成如下形式：（假設(shè)類(lèi)名為實(shí)體類(lèi)Entity，ENTITY為一實(shí)體集合，T1——Tn都是T類(lèi)型的子類(lèi)型）

MACHINE Entity

SETS

ENTITY

VARIABLES

Entities，

Att1，att2，...，attn

INVARIANT

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

...

END［３］

該機(jī)器是一組Entity實(shí)例的模型，而不是一個(gè)單獨(dú)的實(shí)體。集合ENTITY代表Entity實(shí)例的所有可能同類(lèi)體的集合，entities代表當(dāng)前已有的Entity實(shí)例的對(duì)象同類(lèi)體集合。Entity實(shí)例的標(biāo)準(zhǔn)創(chuàng)建操作為：

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［４］

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

MACHINE Entity

SEES Entity2，Entity3，...

...

END

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

我們還可以使用一個(gè)參數(shù)對(duì)一個(gè)將允許的給定實(shí)體的最大實(shí)例數(shù)給出限制：

MACHINE Entity (maxEntity)

CONSTRAINTS

maxEntity≥1

...

PROPERTIES

Card (ENTITY)=maxEntity

INVARIANT

Entities?哿ENTITY ...

END

如果Entity2繼承Entity1，那么需要把約束entities2 ( entities1放在標(biāo)識(shí)超類(lèi)的機(jī)器不變式中。

MACHINE Entity1

SETS

ENTITY1

VARIABLES

entities1，entities2

INVARIANT

entities1?哿ENTITY1(

entities2 ?哿entities1

...

END［２］

4.結(jié)語(yǔ)

本文討論如何讓用B方法來(lái)描述UML類(lèi)圖，從而為提高軟件開(kāi)發(fā)的效率、降低成本打下了基礎(chǔ)，并能大大地改善軟件工程的質(zhì)量。

參考文獻(xiàn)：

［1］裘宗燕譯.Ｂ方法.電子工業(yè)出版社，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］鄒盛榮，鄭國(guó)梁.B語(yǔ)言和方法與Z、VDM的比較.計(jì)算機(jī)科學(xué)，2002（10）：136-138.

［6］鄒盛榮，鄭國(guó)梁.形式化方法B和UML的結(jié)合研究.中國(guó)科技論文在線，2003中國(guó)計(jì)算機(jī)大會(huì).