摘要 本文從初始需求開始構建聊天室模型
以及對個案進行研究
在不同的開發階段
分別要用到UML類圖
時序圖和狀態圖
這樣
難免需要確定一致性問題
現在已經提出了許多仿真和方法
用來確保模型各個方面的一致性
我們關注內部一致性
即給定模型內部制品之間的一致性問題
簡介 軟件系統的開發過程通常會被劃分成一些步驟
每個步驟會用到不同的UML圖
由於建模系統變得越來越復雜
一致性問題就越發突出起來
而在其中
有兩種類型或問題更為顯著
第一
內部一致性問題
涉及給定模型內部制品之間的一致性
第二
系統之間一致性問題
涉及軟件開發過程中不同演化模型之間的一致性
我們主要關注於內部一致性問題
不同的文獻提出了不同的形式化方法
用來自動檢查一致性
發現設計當中存在的問題
在下面幾節裡
我們分步研究了一個聊天室的開發過程
本文的靈感來源於Agder大學Geir Melby完成的一次項目報告（）
這個模型提出了一些潛在的一致性問題
對於它們當中的部分內容
也給出了自動化的一致性檢查方法
在這份案例研究中
我們從需求開始開發了一個聊天室模型
第二節給出了客戶
管理器對象以及聊天室之間的通信協議
作為初始需求
第三節研究了一個可能的類的設計
它定義了符合協議的接口
第四節中給出的時序圖進一步定義和描述了組件之間的通信
並保持與類設計之間的一致性
第五節使用狀態圖更進一步地確定應用程序的行為
這份規程可以在我們的SVM（狀態圖虛擬機）環境中實時地進行仿真或執行
在第六節中
討論了協議規程與仿真跡的一致性
第七節進行總結
通信協議 我們將要創建的聊天室程序是按照客戶機/服務器范型來架構的
客戶會隨機連接聊天室
如果某個聊天室接收了客戶
客戶就會發送消息給這個聊天室
然後聊天室廣播每條消息
除了發送者以外
每個與聊天室建立連接的客戶都會收到一份拷貝
下面將要描述一個特定的簡化了的用例
X 系統包括五個客戶和兩個聊天室
客戶端最初沒有連接
每隔一到三秒（非均勻分布）
它們都會隨機連接一個聊天室
被請求的聊天室同時收到請求（假定沒有網絡延時
並且通信可靠）
X 一個聊天室至多接收三個客戶
當且僅當容量沒有超標時聊天室才會接收連接
X 發出請求的客戶會立刻收到接收或拒絕通知
X 在客戶可以發送聊天信息之前必須被一個聊天室接收
X 連接建立之後
客戶會每隔一到五秒（非均勻分布）給它所連接的聊天室發送隨機消息
聊天室會立即接收消息
它將耗時一秒鐘來處理接收到的消息
並把它廣播給除發送者之外的所有連接客戶
X 客戶會同時收到廣播
為了簡化起見
我們不討論沒有連接的情況
類的設計 根據上面的規定
顯然我們需要兩個類
Client和ChatRoom
在開發過程早期階段
對於仿真來說無需用戶干預
我們明確地按照隨機過程對用戶行為（連接請求和聊天信息）進行建模
以後
客戶模型將會被與軟件打交道的真實客戶所代替
仿真開始時
會初始化五個Client實例和兩個ChatRoom實例
我們還加入了一個singleton類
Manager
Manager以仲裁者的身份中繼組件之間的所有通信
這種中央控制措施將會幫助截取系統傳遞的所有消息
使用它們就可以檢查模型的正確性
圖一描述了由這三個類組成的UML類圖
X ChatRoom提供兩個方法處理到達的事件
request處理來到的請求
每個請求都有參數clientID和roomID
ChatRoom把接收或拒絕通知發回擁有全局ID標識clientID的發送者
它也使用參數roomID來決定請求是發給它自己還是發給另外一個聊天室了
send方法接收由客戶clientID發送的消息msg
這條msg將會在一秒鐘之後被廣播出去
X Client的方法accept和reject處理到達的接收和拒絕通知
參數clientID用來確定目標客戶
當一個Client接收到一個broadcast事件
它會檢查自己是否在clients集合中
如果情況確實如此
消息msg就會在輸出中被打印出來
X Manager中繼連接請求
接收和拒絕通知
來自客戶的消息以及聊天室的廣播
例如
如果它收到來自聊天室的廣播
有三個參數會告訴它消息最初的發送者（客戶）
廣播者（聊天室）以及消息字符串
然後它把消息發給所有連接在聊天室中的
除了最初發送者以外的客戶
圖一 類的設計 盡管這種API定義不是形式化的
但接口背後的行為還是很容易理解的
但是
檢查協議的一致性會有些困難
甚至是不可能的
原因如下
X 行為隱藏在接口背後
它只能在理解的基礎上進行解釋
X 協議是用自然語言表達的
程序不可能很容易地處理
X 對於一個定義完好的系統來說
會有許多接口設計
它們可能有相當大的不同
例如
本設計中用Manager類來攔截通信
另一項設計可能會使用RequestManager來攔截請求
接收和拒絕
用MessageManager來攔截消息和發送廣播
更有另外一種設計可能根本就不會使用任何管理器
時序圖 本節討論的時序圖把設計帶入比類圖更低的抽象層次（更高層次的細節）
時序圖必須清晰反映組件之間的交互
圖二 請求模式的時序圖
圖三 消息模式的時序圖 定時
定時問題使得協議轉化為時序圖和之後轉化為狀態圖的過程變得困難
在協議描述中
同一時刻會發生一個或多個動作
即使這些動作在某種原因下相關也是如此
例如
聊天室不應該在收到請求之前發送接收或拒絕消息
這樣的話
輸出跡中出現
在時刻
請求
在時刻
接收
就是正確的
如果出現
在時刻
接收
在時刻
請請求
那就是不正確的
一種可能的解決方案是使用tuple(t
s)表示時間
t是以秒計數的浮點時間
s是整數序號
以這種方式
正確的輸出可以寫成
在時刻(
s
)請求
在時刻(
s
)接收
序列
在時刻(
s
)接收
在時刻(
s
)請求
則是不正確的
請求和消息模式
請求模式如圖二所示
Client首先會調用Manager的方法mrequest
然後Manager通過調用ChatRoom的方法request中繼這個調用
ChatRoom立刻響應
回調Manager的方法maccept或mreject
然後請求Client會接收到由Manager中繼的響應
圖三是消息模式
在系統中隨機產生消息
進行傳遞
注意ChatRoom在收到一次請求後故意延時一秒鐘
在這兩個時序圖中
沒有其它延時存在
類圖和協議之間的一致性問題
與類圖之間的一致性是容易檢查的
可以通過收集組件接收到的所有方法調用來達成
例如
在請求模式中
Manager接收mrequest
maccept和mreject
在消息模式中
它接收msend和mbroadcast
這五個方法在類圖中都有定義
但沒有定義其它的公有方法
由於時序圖中並沒有給出參數
那樣就沒有檢查參數的必要
檢查過程可以自動化
可以部分檢查協議的一致性
從請求時序圖中很容易就能看出
聊天室在時刻
收到一個請求
在時刻
接收或拒絕這個客戶
這兩個時刻的絕對值並不重要
重要的是
回復確實會在同一時間發回
這樣設計者就可以手工檢查
某個時間應該會發生什麼
如果用到後面討論的基於規則的方法
有限的自動檢查也是可以做到的
注意基本的時序圖無法表達某個時間或某個階段不應該發生的事情
比方說
協議中會含有這樣的意思
聊天室在沒有收到請求時不會接收或拒絕客戶
時序圖中不會包含這樣的信息
這會在模型中帶來設計錯誤
影響後續開發步驟的正確性
另一種可能的設計錯誤是時序圖的語義
例如
在請求模式中
時序圖描述
如果客戶發送mrequest
管理器沒有時間前置地發送request
聊天室發送maccept或mreject
也沒有時間前置
然後管理器發送accept或reject
不幸地是
遲鈍的客戶不會發送任何請求
這顯然是系統當中的一個問題
不能通過檢查時序圖檢測出來
最壞的情況是根本沒有客戶連接
這樣系統就會永遠停機
為了補償信息丟失
需要UML形式化體系中的其它設計
它們並不完全依賴時序圖
或者就要對時序圖進行擴展
一個極好的使用時序圖並引入擴展的例子是Live Sequence Charts
參見Harel的文章[
]
狀態圖 狀態圖用來實現類定義背後的行為
它們可以在我們的SVM（狀態虛擬機）[
][
]中執行
用於擴展狀態圖形式化的解釋器是用Python編寫的
SVM約定
如果想要輕松理解狀態圖設計
就必須先了解SVM的一些約定
SVM用擴展狀態圖形式化體系解釋模型
加入了一些新的功能
盡管表現力沒有加強
但易用性卻大大改進了
盡管最初的狀態圖並不是模塊化的
但仍然可以使用SVM實現基於組件的設計
對於聊天室模型來說這是必需的
象客戶和聊天室這樣的組件可以獨立進行設計
但最終在系統中還是要一起工作的
組件通過導入可以進行復用
較大的組件導入一些小的組件（實例）
作為它的一個狀態
結果是
就象被導入組件的所有狀態（分層的）和轉換都是直接在這個狀態當中編寫一樣
SVM模型用文本文件編寫
宏是在SVM中引入的一個概念
宏在SVM源文件裡的MACRO節中定義
一旦定義後
在整個文本文件中就可以括在括號中使用
例如
定義PREFIX=state
[PREFIX]就可以用來代替字符串
state
這樣[PREFIX]
就等於state
後面就會用到其中的一些預定義宏
[EVENT(event
param)]會觸發一次事件
它的參數是字符串event和可選列表param
[PARAM]用來檢索在處理的事件的參數
它通常在監視哨單元或轉換的輸出中使用
[DUMP(msg)]打印調試信息或在文本文件中記錄這些信息
組件被導入的時候宏也可以充當參數
進行導入的組件要重新定義一部分或所有最初在被導入組件中定義的宏
也包括預定義宏
繼續前面的例子
如果進行導入的組件確定PREFIX=mystate作為導入參數
被導入組件中的[PREFIX]
將會譯為mystate
很容易就可以看出
這些擴展並沒有增加狀態圖的表現力
擴展狀態圖形式體系中的聊天室模型
Client
ChatRoom和Manager組件分別在獨立的狀態圖中設計
如圖四所示
Chat模型導入了五個Client實例
兩個ChatRoom實例和一個Manager實例
同一類型的每個實例都有一個惟一的ID參數
由於可接收的事件集合是不相交的
因此不同類型的實例就可以擁有相同的ID
這個模型可以在SVM環境中仿真或執行
Client組件如圖五所示
最初
它處在nochat狀態
每隔一到三秒（非均勻分布）會觸發一次mrequest事件
通過管理器來重復連接聊天室
直到請求被接收為止（accept事件被接收）
uniform是一個Python函數
它返回某個區間內的隨機實數值
randint返回隨機整數值
事件的第一個參數給出客戶的惟一ID
第二個參數給出目的聊天室（隨機從
或
中選取）
然後
客戶轉移到狀態connected
開始發送消息和接收廣播
事件參數是作為列表發送的
[PARAM][
]訪問第一個參數
依次類推
注意
當方括號之間的內容不是宏的名字或Python下標時
那它就是監視哨
遵循最初狀態圖形式化體系中的定義[
]
用戶定義的宏[ID]為每個客戶指定一個惟一ID
定義ID=
的意思是缺省值為
它可以由導入組件（在這裡是Chat模型）變為一個惟一數
組件的ID很重要
既然整個系統在導入後可以被看作一幅大的狀態圖
每一個正交組件都能接收到所有的廣播事件
這樣
給特定客戶發送事件的惟一方法是在參數列表中給出接收者的ID
每一個客戶都要檢查在處理事件之前
它的ID是否匹配
與Client組件相比
ChatRoom要更復雜
它使用列表messages[ID]把到來的消息進行排隊
這就意味著每一個有著惟一ID的聊天室都會有其自己的隊列（如果ID=
messages[ID]與message
相等）
如果當它正在處理前面的消息時（要耗時一秒鐘）
一條消息到達
新到達的消息就會加入列表之中
收到消息時的時間也被記錄下來
這樣即使消息進行排隊
它的處理時間自到達時開始計算仍為一秒鐘
Manager組件僅僅只是中繼消息
在聊天室接收客戶時
函數rec_comm(client
room)在一個列表中記錄連接信息
get_clients(room
client)查詢列表並返回聊天室room中除了client以外的所有客戶
get_room(client)返回client的房間ID號
聊天室消息隊列和管理器連接列表是變量使用示例
它們幫助記錄模型的狀態
嚴格地說
這仍舊是對最初狀態圖的擴展
狀態必須明確地確定下來
討論變量已經超出了本次個案研究的范圍
與類圖之間的一致性
基於組件的設計應該嚴格符合圖一中的類設計
再者
組件可以發送事件給接收者
但接收者卻不能處理它
或者
發送者提供的參數可能會比需要的要少
這可能會造成嚴重的運行時錯誤
自動檢查所有方法調用的發送者
接收者之間的一致性
這樣的程序可以寫出來
而不是要編寫如何在代碼級由類型檢查器和/或鏈接器來檢查一致性
譬如
Manager接收事件maccept
這意味著它在類定義中提供方法maccept
在處理事件的狀態轉換輸出和監視哨中
要用到[PARAMS][
]和[PARAMS][
]
這樣它就至少需要兩個參數
檢查器遍歷整個Chat模型
找出僅由ChatRoom組件調用（異步地）的方法
調用[EVENT(
maccept
[[PARAMS][
]
[ID]])]提供了兩個參數（[PARAMS][
]
和[ID]）
檢查這條調用是成功的
同樣地
在模型中所有方法調用的一致性可以由狀態圖來檢查
模型執行進行的一致性檢查 SVM解釋器可以仿真或實時（循環中有人參與的情況下需要）執行Chat模型
執行後的輸出結果被轉儲顯示並拷貝一份到文本文件
正如上面說的那樣
如果所有的用戶交互都明確建模的話
根本就不需要干預
輸出跡是我們驗證執行結果的惟一方法
必須檢查所有設計制品與輸出跡之間的一致性
類圖一致性在前面一節中已經研究過
檢查器形式化地檢查狀態圖設計
不需要模型執行
時序圖一致性可以通過驗證實驗輸出跡來檢查
盡管許多情況下正確性仍然不能得到驗證（搜索較大范圍或者有可能無限狀態空間的可能行為）
但對最終產品的信心還是大大增加了
狀態圖一致性含有假定SVM執行環境正確的意思
使用最初的協議驗證一致性並不容易
因為它比時序圖包含更多的信息
檢查程序處理起來會非常困難
圖四 Chat模型
圖五 Client組件
圖六 聊天室組件
圖七 管理器組件 輸出跡
宏[DUMP(msg)]用來在文件中記錄消息msg
一直到執行結束為止（或者自動
或者由調試器手動控制）
每條消息包括三個部分
時間tuple(t
s)
有著惟一ID的發送者或接收者
和消息體
下面是從輸出中截取的一部分內容
CLOCK: (
s
)
Client
Says
Hello!
to ChatRoom
CLOCK: (
s
)
ChatRoom
Broadcasts
Hello!
to all clients except
Client
CLOCK: (
s
)
Client
Receives
Hello!
from Client
管理器產生輸出
它可以訪問通信過程中的所有信息
ID為
的客戶在時刻
發送了一條消息
根據協議
號聊天室在一秒鐘後把該消息廣播出去
另一個連接在
號聊天室的客戶
在同一時刻收到消息
這裡也可以看出消息的最初發送者
與時序圖的一致性
與時序圖的一致性可以通過一套基於規則的方法檢查
這些規則在文本文件中定義
檢查程序讀取文件
檢查輸出跡是否可以滿足所有的規則
正則表達式被擴展之後用以描述規則
規則由四部分組成
前置條件
後置條件
監視哨（任選）和計數規則屬性（任選）
前置條件是正則表達式
用來匹配部分輸出跡
它與監視哨（一個布爾表達式）結合
定義何時可以使用規則
當規則可用
並且計數規則屬性為false時
後置條件（另一個正則表達式）必須要在輸出跡中找到
如果計數規則屬性為true
後置條件一定不可滿足
例如
下面的規則就說明了消息的發送者並沒有在一秒鐘後收到廣播
前置條件
CLOCK: \((\d+\
{
}\d*)s
(\d+\
{
}\d*)\)\n\Client (\d+)\nSays
(
*?)
to ChatRoom (\d+)\n
後置條件
CLOCK: \([(\
+
)]s
(\d+\
{
}\d*)\)\nClient [(\
)]\n Receives
[(\
)]
from Client [(\
)]\n
監視哨
[(\
+
)]<50
計數規則
True
在前置條件中，在括號中定義了五個表達式分組。TW.WinGwIT.Com分別編號從1到5。組1匹配浮點時間。組2匹配序號。它們組成時間元組。組3匹配以整數標記的發送者的客戶ID。組4匹配消息，它可以是任意的字符串。組5匹配發送者所在的聊天室。
在後置條件中，[(…)]包含一個表達式，分組值可以在 “\”後使用索引號來引用。這樣，[(\1+1)]是第一個組的值加一。[(\3)]等於組3。關於正則表達式的更多內容可以在[5]中找到。
假定執行過程停止在仿真時刻50那裡，檢查就不應該超過時刻50。在沒有額外條件的情況下，如果在時刻49.5一條消息發送到聊天室，檢查程序會希望在時刻50.5時見到相應的廣播。為了實現這項功能，引入了一個監視哨[(\1+1)]<50。它會告知檢查程序這條規則僅在分組1的值加一小於50時可用。
客戶不應該接收到它自己的消息，這就是一條計數規則。
6.3 與協議的一致性
驗證模型與協議完全一致如果說是並非不可能的話，至少也是極為困難的。協議，也可以看成需求集合，是使用自然語言描述的。准確解釋它是自動檢查程序開發的主要障礙。
你可能會爭辯說協議可以轉換為一套規則。使用上面描述的基於規則的方法，協議一致性就可以檢查。但是，把協議的完整含義轉化為程序易於處理的形式化表達是非常困難的。協議中含有的明顯事實和常識常常會丟失。作為人與程序之間的接口，自然語言處理技術是有必要的。
在這個案例中，采用了一系列步驟來達成最終的可執行設計。在把協議轉換為另一種不同的形式化表達體系時，信息就會丟失。中間步驟檢查並不能保證最終產品的正確性。
另一方面，檢查中間步驟並不足夠有效。再者說，根據初始協議直接檢查模型是極端困難的事情。在這個案例中，“如何驗證最終設計的正確性”是最後的，同時也是最大的公開問題。
7 結論 在這個案例研究中，我們對一個具體的例子進行了討論。從初始需求開始，我們開發了一個可執行程序。此間經歷一些步驟，在不同的抽象層次上進行設計。我們挑選了一種基於組件的方法來把模型模塊化，並使模型可以管理。類圖定義了組件的接口。盡管只是部分闡述了需求，時序圖形式化通信，使得自動檢查變為可能。在擴展狀態圖形式化體系中，我們建模了基於組件的模型，這個模型由SVM執行環境直接轉換。開發聊天室模型會引起一系列一致性問題。對於其中一部分內容，可以成功運用自動檢查功能。
1． 時序圖與類圖間的一致性得到了檢查。檢查程序驗證所有的必需方法在接口中都已正確地確定下來。
2． 狀態圖與類圖間的一致性也可按照同樣的方法檢查。事件的發送者總能為接收者提供足夠的參數。
3． 狀態圖與時序圖間的一致性使用基於規則的檢查程序來檢查。正則表達式被擴展用來確定前置條件、後置條件、監視哨和計數規則屬性。
然而，還有一些一致性問題仍然沒有解決。
1． 類圖與協議（初始需求）之間的一致性沒有檢查。在後續步驟中會發現設計缺陷，或者缺陷也可能會隱藏在最終產品裡面。
2． 時序圖與協議之間的一致性僅僅做了手工檢查。盡管時序圖只是協議的形式化方法，編寫一個程序檢查它的正確性也並不容易。
3． 檢查擴展狀態圖中的最終設計和協議之間的一致性，要更為困難。這種檢查是必要的，但信息在中間步驟有丟失現象。
應該把注意力放在這些開放問題上，它們大多與系統之間的一致性有關。一致性檢查應該是開發過程中和軟件開發工具的一個完整的組成部分。
參考文獻 [1] D. Harel and R. Marelly. Specifying and executing behavioral requirements: The play-in/play-out approach. Technical Report MSC01-15, The Weizmann Institute of Science, 2001.
[2] Thomas Feng. An extended semantics for a Statechart Virtual Machine. In A. Bruzzone and hamed Itmi, editors, Summer Computer Simulation Conference. Student Workshop, pages S147 ? S166. The Society for Computer Modelling and Simulation, July 2003. Montr′eal, Canada.
[3] Thomas Feng. Statechart Virtual Machine (SVM), 2003. MSDL, McGill University,
[4] David Harel and Amnon Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293?333, 1996.
[5] Python 2.2.3 documentation, May 2003.
[6] David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231?274, June 1987.
[7] Michael von der Beeck. A structured operational semantics for UML statecharts. Software and Systems Modeling, 1(2), 2002.
[8] Jim Rumbaugh, Ivar Jacobson, and Grady Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1998.
1UML狀態圖（UML 2.0以前的版本）在後面步驟中會用到，它不允許確定事件的接收者，即使只有一個聊天室會處理事件，所有的聊天室也同樣都會收到相同的請求。
2為了增強表達能力，可以引入某些擴展，但這樣的話檢查模型的正確性將變得更加困難。
3這裡[PARAM][0]的指的是事件請求的第一個參數，它可以由ChatRoom組件來處理。這個參數會進一步在事件maccept中傳遞，它是後者的第一個參數。
From:http://tw.wingwit.com/Article/program/Java/gj/201311/27494.html
