摘要
本文從初始需求開始構建聊天室模型,以及對個案進行研究.在不同的開發階段,分別要用到UML類圖、時序圖和狀態圖.這樣,難免需要確定一致性問題,現在已經提出了許多模擬和方法,用來確保模型各個方面的一致性.我們關注內部一致性,即給定模型內部製品之間的一致性問題.
1 簡介
軟體系統的開發過程通常會被劃分成一些步驟,每個步驟會用到不同的UML圖.由於建模系統變得越來越複雜,一致性問題就越發突出起來.而在其中,有兩種類型或問題更為顯著.第一,內部一致性問題,涉及給定模型內部製品之間的一致性.第二,系統之間一致性問題,涉及軟體開發過程中不同演化模型之間的一致性.我們主要關注於內部一致性問題.
不同的文獻提出了不同的形式化方法,用來自動檢查一致性,發現設計當中存在的問題.在下面幾節里,我們分步研究了一個聊天室的開發過程.本文的靈感來源於Agder大學Geir Melby完成的一次項目報告（http://fag.grm.hia.no/ikt2340/year2002/）.這個模型提出了一些潛在的一致性問題.對於它們當中的部分內容,也給出了自動化的一致性檢查方法.
在這份案例研究中,我們從需求開始開發了一個聊天室模型.第二節給出了客戶、管理器對象以及聊天室之間的通信協議,作為初始需求.第三節研究了一個可能的類的設計,它定義了符合協議的介面.第四節中給出的時序圖進一步定義和描述了組件之間的通信,並保持與類設計之間的一致性.第五節使用狀態圖更進一步地確定應用程序的行為.這份規程可以在我們的SVM（狀態圖虛擬機）環境中實時地進行模擬或執行.在第六節中,討論了協議規程與模擬跡的一致性.第七節進行總結.
2 通信協議
我們將要創建的聊天室程序是按照客戶機/伺服器范型來架構的.客戶會隨機連接聊天室.如果某個聊天室接收了客戶,客戶就會發送消息給這個聊天室.然後聊天室廣播每條消息,除了發送者以外,每個與聊天室建立連接的客戶都會收到一份拷貝.
下面將要描述一個特定的簡化了的用例：
X 系統包括五個客戶和兩個聊天室.客戶端最初沒有連接.每隔一到三秒（非均勻分佈）,它們都會隨機連接一個聊天室.被請求的聊天室同時收到請求（假定沒有網路延時,並且通信可靠）.
X 一個聊天室至多接收三個客戶.當且僅當容量沒有超標時聊天室才會接收連接.
X 發出請求的客戶會立刻收到接收或拒絕通知.
X 在客戶可以發送聊天信息之前必須被一個聊天室接收.
X 連接建立之後,客戶會每隔一到五秒（非均勻分佈）給它所連接的聊天室發送隨機消息.聊天室會立即接收消息,它將耗時一秒鐘來處理接收到的消息,並把它廣播給除發送者之外的所有連接客戶.
X 客戶會同時收到廣播.為了簡化起見,我們不討論沒有連接的情況.
3 類的設計
根據上面的規定,顯然我們需要兩個類：Client和ChatRoom.在開發過程早期階段,對於模擬來說無需用戶干預,我們明確地按照隨機過程對用戶行為（連接請求和聊天信息）進行建模.以後,客戶模型將會被與軟體打交道的真實客戶所代替.模擬開始時,會初始化五個Client實例和兩個ChatRoom實例.
我們還加入了一個singleton類：Manager.Manager以仲裁者的身份中繼組件之間的所有通信.這種中央控制措施將會幫助截取系統傳遞的所有消息,使用它們就可以檢查模型的正確性.
圖一描述了由這三個類組成的UML類圖.
X ChatRoom提供兩個方法處理到達的事件.request處理來到的請求,每個請求都有參數clientID和roomID.ChatRoom把接收或拒絕通知發回擁有全局ID標識clientID的發送者.它也使用參數roomID來決定請求是發給它自己還是發給另外一個聊天室了1.send方法接收由客戶clientID發送的消息msg.這條msg將會在一秒鐘之後被廣播出去.
X Client的方法accept和reject處理到達的接收和拒絕通知.參數clientID用來確定目標客戶.當一個Client接收到一個broadcast事件,它會檢查自己是否在clients集合中.如果情況確實如此,消息msg就會在輸出中被列印出來.
X Manager中繼連接請求、接收和拒絕通知、來自客戶的消息以及聊天室的廣播.例如,如果它收到來自聊天室的廣播,有三個參數會告訴它消息最初的發送者（客戶）,廣播者（聊天室）以及消息字元串.然後它把消息發給所有連接在聊天室中的,除了最初發送者以外的客戶.
圖一 類的設計 儘管這種API定義不是形式化的,但介面背後的行為還是很容易理解的.但是,檢查協議的一致性會有些困難,甚至是不可能的,原因如下：
X 行為隱藏在介面背後,它只能在理解的基礎上進行解釋.
X 協議是用自然語言表達的,程序不可能很容易地處理.
X 對於一個定義完好的系統來說,會有許多介面設計.它們可能有相當大的不同.例如,本設計中用Manager類來攔截通信.另一項設計可能會使用RequestManager來攔截請求、接收和拒絕,用MessageManager來攔截消息和發送廣播.更有另外一種設計可能根本就不會使用任何管理器.
4 時序圖
本節討論的時序圖把設計帶入比類圖更低的抽象層次（更高層次的細節）.時序圖必須清晰反映組件之間的交互.
圖二 請求模式的時序圖
圖三 消息模式的時序圖 4.1 定時
定時問題是的協議轉化為時序圖和之後轉化為狀態圖的過程變得困難.在協議描述中,同一時刻會發生一個或多個動作,即使這些動作在某種原因下相關也是如此.例如,聊天室不應該在收到請求之前發送接收或拒絕消息.這樣的話,輸出跡中出現「在時刻1請求；在時刻1接收」就是正確的,如果出現「在時刻1接收；在時刻1請請求」,那就是不正確的.
一種可能的解決方案是使用tuple(t, s)表示時間,t是以秒計數的浮點時間,s是整數序號.以這種方式,正確的輸出可以寫成「在時刻(1.0s, 0)請求；在時刻(1.0s, 1)接收」.序列「在時刻(1.0s, 0)接收；在時刻(1.0s, 1)請求」則是不正確的.
4.2 請求和消息模式
請求模式如圖二所示.Client
會調用Manager的方法mrequest.然後Manager通過調用ChatRoom的方法request中繼這個調用.ChatRoom立刻響應,回調Manager的方法maccept或mreject.然後請求Client會接收到由Manager中繼的響應.
圖三是消息模式,在系統中隨機產生消息,進行傳遞.注意ChatRoom在收到一次請求后故意延時一秒鐘.在這兩個時序圖中,沒有其它延時存在.
4.3 類圖和協議之間的一致性問題
與類圖之間的一致性是容易檢查的,可以通過收集組件接收到的所有方法調用來達成.例如,在請求模式中,Manager接收mrequest、maccept和mreject.在消息模式中,它接收msend和mbroadcast.這五個方法在類圖中都有定義,但沒有定義其它的公有方法.由於時序圖中並沒有給出參數,那樣就沒有檢查參數的必要.檢查過程可以自動化.可以部分檢查協議的一致性.從請求時序圖中很容易就能看出,聊天室在時刻0收到一個請求,在時刻0接收或拒絕這個客戶.這兩個時刻的絕對值並不重要.重要的是,回復確實會在同一時間發回.這樣設計者就可以手工檢查「某個時間應該會發生什麼」.如果用到後面討論的基於規則的方法,有限的自動檢查也是可以做到的.
注意基本的時序圖無法表達某個時間或某個階段不應該發生的事情.比方說,協議中會含有這樣的意思,聊天室在沒有收到請求時不會接收或拒絕客戶.時序圖中不會包含這樣的信息.這會在模型中帶來設計錯誤,影響後續開發步驟的正確性.另一種可能的設計錯誤是時序圖的語義.例如,在請求模式中,時序圖描述：如果客戶發送mrequest,管理器沒有時間前置地發送request,聊天室發送maccept或mreject,也沒有時間前置,然後管理器發送accept或reject.不幸地是,遲鈍的客戶不會發送任何請求,這顯然是系統當中的一個問題,不能通過檢查時序圖檢測出來.最壞的情況是根本沒有客戶連接,這樣系統就會永遠停機.為了補償信息丟失,需要UML形式化體系中的其它設計,它們並不完全依賴時序圖,或者就要對時序圖進行擴展.一個極好的使用時序圖並引入擴展的例子是Live Sequence Charts,參見Harel的文章[1].
5 狀態圖
狀態圖用來實現類定義背後的行為.它們可以在我們的SVM（狀態虛擬機）[2][3]中執行,用於擴展狀態圖形式化的解釋器是用Python編寫的.
5.1 SVM約定
如果想要輕鬆理解狀態圖設計,就必須先了解SVM的一些約定.
SVM用擴展狀態圖形式化體系解釋模型.加入了一些新的功能,儘管表現力沒有加強2,但易用性卻大大改進了.
儘管最初的狀態圖並不是模塊化的,但仍然可以使用SVM實現基於組件的設計.對於聊天室模型來說這是必需的,象客戶和聊天室這樣的組件可以獨立進行設計,但最終在系統中還是要一起工作的.組件通過導入可以進行復用.較大的組件導入一些小的組件（實例）,作為它的一個狀態.結果是,就象被導入組件的所有狀態（分層的）和轉換都是直接在這個狀態當中編寫一樣.
SVM模型用文本文件編寫.宏是在SVM中引入的一個概念.宏在SVM源文件里的MACRO節中定義.一旦定義后,在整個文本文件中就可以括在括弧中使用.例如,定義PREFIX=state,[PREFIX]就可以用來代替字元串「state」,這樣[PREFIX]1就等於state1.
後面就會用到其中的一些預定義宏.[EVENT(event, param)]會觸發一次事件.它的參數是字元串event和可選列表param.[PARAM]用來檢索在處理的事件的參數.它通常在監視哨單元或轉換的輸出中使用.[DUMP(msg)]列印調試信息或在文本文件中記錄這些信息.
組件被導入的時候宏也可以充當參數.進行導入的組件要重新定義一部分或所有最初在被導入組件中定義的宏,也包括預定義宏.繼續前面的例子,如果進行導入的組件確定PREFIX=mystate作為導入參數,被導入組件中的[PREFIX]1將會譯為mystate1.
很容易就可以看出,這些擴展並沒有增加狀態圖的表現力.
5.2 擴展狀態圖形式體系中的聊天室模型
Client、ChatRoom和Manager組件分別在獨立的狀態圖中設計.如圖四所示,Chat模型導入了五個Client實例,兩個ChatRoom實例和一個Manager實例.同一類型的每個實例都有一個惟一的ID參數.由於可接收的事件集合是不相交的,因此不同類型的實例就可以擁有相同的ID.這個模型可以在SVM環境中模擬或執行.
Client組件如圖五所示.最初,它處在nochat狀態.每隔一到三秒（非均勻分佈）會觸發一次mrequest事件,通過管理器來重複連接聊天室,直到請求被接收為止（accept事件被接收）.uniform是一個Python函數,它返回某個區間內的隨機實數值,randint返回隨機整數值.事件的第一個參數給出客戶的惟一ID.第二個參數給出目的聊天室（隨機從1或2中選取）.然後,客戶轉移到狀態connected,開始發送消息和接收廣播.事件參數是作為列表發送的,[PARAM][0]訪問第一個參數,依次類推.注意,當方括弧之間的內容不是宏的名字或Python下標時,那它就是監視哨,遵循最初狀態圖形式化體系中的定義[4].
用戶定義的宏[ID]為每個客戶指定一個惟一ID.定義ID=0的意思是預設值為0.它可以由導入組件（在這裡是Chat模型）變為一個惟一數.組件的ID很重要.既然整個系統在導入后可以被看作一幅大的狀態圖,每一個正交組件都能接收到所有的廣播事件.這樣,給特定客戶發送事件的惟一方法是在參數列表中給出接收者的ID.每一個客戶都要檢查在處理事件之前,它的ID是否匹配.
與Client組件相比,ChatRoom要更複雜.它使用列表messages[ID]把到來的消息進行排隊.這就意味著每一個有著惟一ID的聊天室都會有其自己的隊列（如果ID=0,messages[ID]與message0相等）.如果當它正在處理前面的消息時（要耗時一秒鐘）,一條消息到達,新到達的消息就會加入列表之中.收到消息時的時間也被記錄下來,這樣即使消息進行排隊,它的處理時間自到達時開始計算仍為一秒鐘.
Manager組件僅僅只是中繼消息.在聊天室接收客戶時,函數rec_comm(client, room)在一個列表中記錄連接信息.get_clients(room, client)查詢列表並返回聊天室room中除了client以外的所有客戶.get_room(client)返回client的房間ID號.
聊天室消息隊列和管理器連接列表是變數使用示例.它們幫助記錄模型的狀態.嚴格地說,這仍舊是對最初狀態圖的擴展,狀態必須明確地確定下來.討論變數已經超出了本次個案研究的範圍.
5.3 與類圖之間的一致性
基於組件的設計應該嚴格符合圖一中的類設計.再者,組件可以發送事件給接收者,但接收者卻不能處理它.或者,發送者提供的參數可能會比需要的要少.這可能會造成嚴重的運行時錯誤.
自動檢查所有方法調用的發送者-接收者之間的一致性,這樣的程序可以寫出來.而不是要編寫如何在代碼級由類型檢查器和/或鏈接器來檢查一致性.譬如,Manager接收事件maccept.這意味著它在類定義中提供方法maccept.在處理事件的狀態轉換輸出和監視哨中,要用到[PARAMS][0]和[PARAMS][1],這樣它就至少需要兩個參數.檢查器遍歷整個Chat模型,找出僅由ChatRoom組件調用（非同步地）的方法.調用[EVENT("maccept",[[PARAMS][0], [ID]])]提供了兩個參數（[PARAMS][0]3和[ID]）.檢查這條調用是成功的.
同樣地,在模型中所有方法調用的一致性可以由狀態圖來檢查.
6 模型執行進行的一致性檢查
SVM解釋器可以模擬或實時（循環中有人參與的情況下需要）執行Chat模型.執行后的輸出結果被轉儲顯示並拷貝一份到文本文件.正如上面說的那樣,如果所有的用戶交互都明確建模的話,根本就不需要干預.輸出跡是我們驗證執行結果的惟一方法.必須檢查所有設計製品與輸出跡之間的一致性.
類圖一致性在前面一節中已經研究過.檢查器形式化地檢查狀態圖設計.不需要模型執行.時序圖一致性可以通過驗證實驗輸出跡來檢查.儘管許多情況下正確性仍然不能得到驗證（搜索較大範圍或者有可能無限狀態空間的可能行為）,但對最終產品的信心還是大大增加了.
狀態圖一致性含有假定SVM執行環境正確的意思.
使用最初的協議驗證一致性並不容易,
它比時序圖包含更多的信息.檢查程序處理起來會非常困難.
圖四 Chat模型
圖五 Client組件
圖六 聊天室組件
圖七 管理器組件 6.1 輸出跡
宏[DUMP(msg)]用來在文件中記錄消息msg,一直到執行結束為止（或者自動,或者由調試器手動控制）.每條消息包括三個部分：時間tuple(t, s),有著惟一ID的發送者或接收者,和消息體.下面是從輸出中截取的一部分內容：
. . . . . .
CLOCK: (10.5s,0)
Client 0
Says "Hello!" to ChatRoom 1
. . . . . .
CLOCK: (11.5s,0)
ChatRoom 1
Broadcasts "Hello!" to all clients except
Client 0
. . . . . .
CLOCK: (11.5s,2)
Client 1
Receives "Hello!" from Client 0
. . . . . .
管理器產生輸出,它可以訪問通信過程中的所有信息.ID為0的客戶在時刻10.5發送了一條消息.根據協議,1號聊天室在一秒鐘后把該消息廣播出去.另一個連接在1號聊天室的客戶1在同一時刻收到消息.這裡也可以看出消息的最初發送者.
6.2 與時序圖的一致性
與時序圖的一致性可以通過一套基於規則的方法檢查.這些規則在文本文件中定義.檢查程序讀取文件,檢查輸出跡是否可以滿足所有的規則.正則表達式被擴展之後用以描述規則.規則由四部分組成：前置條件、後置條件、監視哨（任選）和計數規則屬性（任選）.前置條件是正則表達式,用來匹配部分輸出跡.它與監視哨（一個布爾表達式）結合,定義何時可以使用規則.當規則可用,並且計數規則屬性為false時,後置條件（另一個正則表達式）必須要在輸出跡中找到；如果計數規則屬性為true,後置條件一定不可滿足.
例如,下面的規則就說明了消息的發送者並沒有在一秒鐘后收到廣播.
前置條件
CLOCK: ((d .{0,1}d*)s,(d .{0,1}d*))nClient (d )nSays "(.*?)" to ChatRoom (d )n
後置條件
CLOCK: ([(1 1)]s,(d .{0,1}d*))nClient [(3)]n Receives"[(4)]" from Client [(3)]n
監視哨
[(1 1)]<50
計數規則
True
在前置條件中,在括弧中定義了五個表達式分組.分別編號從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, http://moncs.cs.mcgill.ca/people/tfeng/?research=svm.
[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. http://www.python.org/doc/2.2.3/.
[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中傳遞,它是後者的第一個參數.
