《軟件架構理論與實踐》 —3.3.2　基于UML的形式化建模方法

3.3.2　基于UML的形式化建模方法

由于軟件架構建模的本質(zhì)在于預先給出待建系統(tǒng)的模型并分析其各種行為和特征，因此如何精確地描述模型顯然是非常重要的。盡管UML可以用于描述軟件架構，對各種軟件系統(tǒng)或離散型系統(tǒng)進行建模，并且通過相應支持工具的配合可進行架構的文檔化和部分目標語言代碼的生成，然而UML不是一種形式化的語言，不能精確地描述系統(tǒng)的運行語義。因此，非形式化描述方法不能支持在軟件架構的抽象模型層面進行相關分析和測試，需要進一步采用形式化建模方法及其支持語言和工具。

形式化方法和UML存在很大的互補性，二者的結合研究對提高軟件架構的建模質(zhì)量有著非常重要的意義。形式化與UML結合的建模過程和UML統(tǒng)一建模過程有明顯的不同，它的目標是直接構造出盡可能正確的系統(tǒng)。圖3-2是形式化與UML結合的開發(fā)過程圖。因為形式化與UML結合的建模過程和UML統(tǒng)一建模過程的目標不同，所以它們的開發(fā)模式也不一樣。形式化與UML結合的建模過程的需求分析和設計階段需要投入大量工作量，通常占到全部工作量的60%～70%，編碼和測試工作則只占30%～40%。而UML統(tǒng)一建模過程的編碼和測試所需工作量非常大，一般要占到60%～70%[63]。從這里可以看出形式化與UML結合的建模過程在需求分析和設計階段所投入的工作量要遠遠大于UML統(tǒng)一建模過程，這主要是因為其在設計階段使用了形式化描述與驗證，保證了軟件架構設計的一致性和可靠性，從而使得后期的編碼和測試工作變得相對簡單。

下面我們來看看如何將形式化方法與UML結合在一起，其中使用的形式化方法以Z語言為例，而UML中以常用的類圖、用例圖、狀態(tài)圖和順序圖為例。

圖3-2　形式化與UML結合的建模過程

1. UML類圖的形式化

UML類圖是由類、泛化和關聯(lián)組成的。類包括屬性和操作，其中操作包含一組有序的參數(shù)。泛化表示了子類和超類的關系。關聯(lián)一般有兩個關聯(lián)端，每個關聯(lián)端具有若干屬性。UML類圖的形式化可以轉(zhuǎn)化為對類、關聯(lián)、泛化的形式化描述[64]。

（1）類的形式化

在UML中，類是一組具有公共特性的對象的抽象。類有名稱、屬性和操作。其中，屬性有名稱、可見性、類型和多重性；操作有名稱、可見性和參數(shù)，操作的每個參數(shù)有名稱和類型。在定義圖形元素之前，先定義幾個集合：Name、Type和Expression。用Z語言表示為[Name, Type, Expression]。在屬性中多重性表示屬性數(shù)據(jù)取值的可能數(shù)目。在UML中可見性可以是私有的、公共的和保護的。如圖3-3所示為類的屬性和參數(shù)的形式化表示。

VisibilityKind::=private丨public丨protected

圖3-3　類的屬性和參數(shù)的形式化表示

操作中的參數(shù)是一個序列，而且參數(shù)名必須唯一。如圖3-4所示。

圖3-4　類的操作的形式化表示

在類中定義的屬性名應該不同，并且操作應該帶有不同的參數(shù)。如圖3-5所示。

圖3-5　類的形式化表示

（2）關聯(lián)的形式化

在UML中，類之間的關系用關聯(lián)來表示。在大多數(shù)情況下，類圖中兩個類之間的關聯(lián)是二元的，而且聚集和組合總是二元關聯(lián)。因此，我們只考慮二元關聯(lián)。二元關聯(lián)有一個關聯(lián)名和兩個關聯(lián)端。每個關聯(lián)端有一個角色名和一個多重性約束、一個描述導航性的屬性和一個描述關系類型（聚集、組合）的屬性。多重性約束描述的非負整數(shù)的范圍表示該位置上可以有多少個對象，并且限制了一端的一個對象可以與另一端的多少個對象有關聯(lián)。謂詞部分的約束表示多重性不能為0，對組合而言，組合端的多重性至多為1。如圖3-6所示為關聯(lián)端的形式化表示。

AggregationKind::=none丨aggregate丨composite

二元關聯(lián)有一個名稱并且恰好有兩個關聯(lián)端。謂詞部分的屬性表示了關聯(lián)的特性：每個角色名必須不同。對聚集和組合關聯(lián)來說，應該只有一個聚集或組合端并且另一端是部分或者聚集值為none。假定e1是聚集或組合端，則關聯(lián)的另一端的聚集值為none，并且屬性名和角色名不重疊。如圖3-7所示。

圖3-6　關聯(lián)端的形式化表示???? 圖3-7　關聯(lián)的形式化表示

（3）泛化的形式化

在UML中，泛化描述了對象之間的分類關系，其中超類對象描述了通用的信息，子類對象描述了特定的信息。如圖3-8所示約束表達式表示不允許循環(huán)繼承。

（4）類圖的形式化

UML類圖是由類、關聯(lián)和泛化組成的。約束表達式表示在類圖中，類的名稱是唯一的，并且關聯(lián)和泛化涉及的類應該在同一個類圖中。如圖3-9所示。

圖3-8　泛化的形式化表示? 圖3-9　類圖的形式化表示

2. UML用例圖的形式化

用例圖由角色、用例和系統(tǒng)三個部分組成，所以對用例圖的形式化工作可轉(zhuǎn)化為對這三種元素的形式化描述[64]。

（1）角色的形式化描述

角色是與系統(tǒng)交互的外部實體（人或事），代表的是一類能使用某個功能的人或事，所以它的形式化描述比較簡單。假設類A和類B使用系統(tǒng)的功能時具有角色C，則角色C可以表示成“Actor C==AVB”。

（2）用例的形式化描述

利用Z語言可以將用例形式化為如圖3-10所示格式。

其中，Use Case Name是模式名，Declarations是聲明部分，Predicates是謂詞不變式部分。對用例模式而言，聲明部分是狀態(tài)變量和輸入/輸出聲明，謂詞不變式是執(zhí)行用例的功能時應滿足的條件和執(zhí)行用例的功能后引起的變化。用例模式的謂詞不變式可以表示如下：

Predicates = Pre-Pred ∩ Post-Pred

不變式中的“∩”表示“并且”的關系，意思是Predicates由Pre-Pred和Post-Pred兩部分組成。Pre-Pred表示執(zhí)行用例的功能前狀態(tài)變量和輸入應滿足的條件，即用例的前置條件；Post-Pred表示執(zhí)行用例的功能后狀態(tài)變量和輸出應滿足的條件，即用例的后置條件。

1）獨立用例的形式化描述：這里的獨立用例是指該用例與其他用例之間不存在use或extend關系。前面所介紹的用例模式可以用來表示獨立用例的形式化，為了更清晰地描述用例模式的前置條件和后置條件，將其用例模式的謂詞不變式部分分成兩部分表示，表示方法如圖3-11所示。

2）有關系的用例的形式化描述：這里有關系的用例指的是與其他用例之間存在擴展或使用關系的用例的形式化。圖3-12是擴展關系和使用關系的用例圖。由于在這兩種關系的用例中，Use Case A均繼承了Use Case B中的一些行為，因此把Use Case B看作父用例，Use Case A看作子用例。形式化描述具有擴展和使用關系的用例時，對于父用例（即Use Case B）將按照獨立用例的形式化方法進行描述；而對于子用例（也就是Use Case A），則將其描述成包含父用例的模式，如圖3-13所示。

圖3-12　具有擴展關系和使用關系的用例圖?????? 圖3-13　有關系的用例圖的形式化表示

相對于獨立用例的形式化，具有擴展和使用關系的用例（子用例）的描述只需要在Declarations部分增加其所繼承的用例的聲明即可。

（3）系統(tǒng)的形式化描述

系統(tǒng)是用例圖的另一個組成部分，它的形式化描述同樣可以按照圖3-13的格式給出，只不過將Use Case Name用System Name代替，如圖3-14所示，圖中System Name是系統(tǒng)的名稱，Declarations是系統(tǒng)所提供的功能（即用例）的聲明，Predicates是對用例的約束，主要用來表示各個用例之間的關系。

（4）用例圖的形式化描述

用例圖是由角色、用例和系統(tǒng)組成的，所以只要將角色、用例和系統(tǒng)的形式化描述組織起來，就可得到用例圖的形式化描述。用例圖的形式化描述如圖3-15所示。圖中，Declarations部分是角色、用例和系統(tǒng)的說明，Predicates部分用于表示角色和用例之間的關系，也就是說用來表示某個角色與哪些用例之間有關系，即使用了用例的功能。

3. UML狀態(tài)圖的形式化

UML狀態(tài)圖由狀態(tài)和遷移組成，對應地，在形式化過程中我們分別定義了遷移模式和狀態(tài)模式，狀態(tài)模式之間的層次化結構機制用Z語言的模式運算來表示[65]。

（1）遷移模式

遷移模式表征一個遷移所引起的狀態(tài)變化，關聯(lián)遷移前的變量值與遷移后的變量值。遷移具有觸發(fā)事件、遷移條件、動作、源狀態(tài)和目標狀態(tài)，在定義Z語言的模式之前，先定義幾個集合：事件集EE、遷移條件集CE、動作集AE。

EE::={Request_Event, Transform_Event, Signal_Event, Time_Event}

CE::={Boolean_Expression}

AE::={Assignment,Call,Create,Destory,Rerurn,Send,Terminate,Uninterpreted}

EE中的事件是具有時間和空間位置的顯著發(fā)生的某件事。事件帶有參數(shù)，參數(shù)可用于遷移中的動作。事件可以劃分為請求事件（Request_Event）、變更事件（Transform_Event）、信號事件（Signal_Event）和時間事件（Time_Event）[66]，如表3-2所示。

表3-2　事件的種類和對應描述

EE中的遷移條件是布爾條件表達式，它可能引用附屬于該狀態(tài)的對象的屬性以及觸發(fā)事件的參數(shù)。遷移條件在觸發(fā)事件發(fā)生時被求值，如果表達式為真，則遷移被激發(fā)。AE中的動作在遷移被激發(fā)時執(zhí)行，動作通常是賦值語句或單個的計算，還包括調(diào)用操作、設置返回值、創(chuàng)建和銷毀對象以及其他指定的控制動作。遷移模式定義如圖3-16所示，其中Name是標識符集合，name指遷移名，Source_state指遷移模式連接的源狀態(tài)模式，TriggerEE指觸發(fā)事件集，Object_state指遷移的目標狀態(tài)模式。

（2）狀態(tài)模式

狀態(tài)模式包含變量聲明和使用聲明變量的謂詞集，其動態(tài)屬性由遷移模式描述，靜態(tài)屬性則由狀態(tài)模式和操作模式來描述，定義如圖3-17所示。

（3）層次化結構機制表示

為了支持大中型軟件開發(fā)，Z語言引入了層次化結構機制，允許用成組框?qū)⑾嚓P的圖元結合在一起，成組框可以嵌套，從而支持對目標軟件系統(tǒng)功能的逐級分解。下面我們利用Z語言的模式運算來定義組合狀態(tài)的狀態(tài)模式，從而表示層次化結構機制。

圖3-17　操作模式以及狀態(tài)模式的形式化表示

狀態(tài)模式之間的OR、AND、SAND三種關系可以分別使用操作符“‖”“&”“#”來定義，其語法為：Schema-Exp::=Schema-Exp op Schema-Exp（其中op為‖、&或#）。

這三個操作符都是二元操作符，操作數(shù)為模式表達式。模式運算定義為合并子模式的變量聲明和斷言以形成一個新的模式。對于‖和&操作符，兩個模式必須類型兼容，#操作符用于描述順序系統(tǒng)，要求兩個模式共享的輸入、輸出變量的類型一致，它的操作效果是對于所有共享變量，第一個模式的輸出值將作為第二個模式的輸入值。在定義了遷移模式和基本狀態(tài)模式S2、S3、S4、S5、S7、S8后，圖3-18中的UML狀態(tài)機示例可用模式運算表示為：

sub1::=S2#S3　sub2::=S4#S5　S6::=S7#S8　S1::=sub1&sub2

S::=S1||S6

圖3-18　UML狀態(tài)機示例

另外S2、S3、S4、S5、S7、S8也可以是引用子狀態(tài)機狀態(tài)或者占位狀態(tài)，可以在逐步求精中不斷細化，外層的狀態(tài)細化成多個內(nèi)部狀態(tài)，每個子狀態(tài)繼承父狀態(tài)的遷移。

4. UML順序圖的形式化

UML順序圖用于描述對象間動態(tài)的交互關系，著重體現(xiàn)對象間消息傳遞的時間順

序[67–68]。順序圖采用兩個軸：水平軸表示不同的實例（其實是角色，每個角色代表一個特定的對象或一組對象的集合，以下稱之為實例），垂直軸表示時間。兩個實例生命線間帶有箭頭的線表示消息，消息的箭頭形狀表明了消息的類型是發(fā)送還是返回。消息按發(fā)生的時間順序從上到下排列，每個消息旁邊標有消息名，也可加上參數(shù)。圖3-19 給出了順序圖的一個具體實例。

圖3-19　用戶成功登錄到服務器的UML順序圖

（1）實例的形式化描述

順序圖具有一定的抽象句法，也必須滿足一些合式規(guī)則。這里使用Z 語言嚴格地對它們進行描述，規(guī)格說明使用了以下給定的類型：[INSTANCE, TYPE, NAME] ，其中INSTANCE、TYPE、NAME分別是所有實例、類型和名稱的集合。

在順序圖中實例的生命線上發(fā)送或接收消息的點稱為位置點，每個實例的生命線上存在著有限個離散的位置點。如圖3-20所示的全程變量

l _max，表示系統(tǒng)所允許的最大位置點。實例生命線上的位置點用模式ILocation 描述，其中任意一個位置點均不大于l_max。

（2）消息的形式化描述

在每個位置點上可以有一個或多個消息發(fā)送給其他實例，或者接收從自身或其他實例發(fā)送過來的一個消息。每個消息上標記有消息的名稱和對應的參數(shù)，其中消息的參數(shù)類型應與系統(tǒng)模型中類圖給出的操作說明一致。為了區(qū)分相同發(fā)送實例和接收實例間激活相同操作的兩個消息，每個消息還附帶一個唯一的標識號。消息標識用模式MsgId描述，其中任意兩個消息的標識號均不相同。如圖3-21所示。

順序圖中可以使用返回標記，它表示從消息處理中返回，而不是一個新消息，所以返回標記與原來的消息具有相同的消息標識。通常情況下它帶有一個返回值，其類型也與類圖中的說明相一致。返回標記可以由模式ReturnId定義，如圖3-22所示。

用S 和R 分別表示消息的發(fā)送和接收，則消息的發(fā)送接收標志MSRFlag 定義為：

MSRFlag ::= S丨R

順序圖中的每個消息與實例生命線上的兩點相關，即發(fā)送消息的位置點和接收消息的位置點，可以用模式Message描述。如圖3-23所示。

另外，用映射msg來描述順序圖中位置與消息之間的對應關系，定義函數(shù)source、target來描述消息與發(fā)送或接收該消息的實例之間的對應關系：

/msg：ILocation??????? F Message

source,target: Message → F1 INSTANCE

順序圖可用模式WFSequenceDiagram描述，其中至少有一個實例和一個消息，并且對于任意的消息，其發(fā)送位置點與接收位置點應不同。如圖3-24所示。

圖3-24　WFSequenceDiagram的形式化描述

UML與Z結合的建模過程是在目前軟件規(guī)模和復雜性不斷增大的情況下提出的，它對現(xiàn)在工業(yè)界軟件架構建模過程做了一些改進，并提出了一些新的思路和構想。不只是Z語言，其他形式化方法也可以將非形式化的UML圖形轉(zhuǎn)換為具有精確語義的形式化規(guī)格說明，在非形式化的圖形表示與形式化定義之間建立映射關系。UML中的類圖、用例圖、狀態(tài)圖以及順序圖較適合形式化描述，用形式化描述方法其他圖反而使得描述過程更加復雜，容易降低效率。

軟件開發(fā) 架構設計 軟件

版權聲明：本文內(nèi)容由網(wǎng)絡用戶投稿，版權歸原作者所有，本站不擁有其著作權，亦不承擔相應法律責任。如果您發(fā)現(xiàn)本站中有涉嫌抄襲或描述失實的內(nèi)容，請聯(lián)系我們jiasou666@gmail.com 處理，核實后本網(wǎng)站將在24小時內(nèi)刪除侵權內(nèi)容。

版權聲明：本文內(nèi)容由網(wǎng)絡用戶投稿，版權歸原作者所有，本站不擁有其著作權，亦不承擔相應法律責任。如果您發(fā)現(xiàn)本站中有涉嫌抄襲或描述失實的內(nèi)容，請聯(lián)系我們jiasou666@gmail.com 處理，核實后本網(wǎng)站將在24小時內(nèi)刪除侵權內(nèi)容。