熱點推薦:
您现在的位置: 電腦知識網 >> 編程 >> Java編程 >> Java高級技術 >> 正文

個案研究:聊天室UML模型一致性問題

2013-11-23 19:48:57  來源: Java高級技術 

  摘要
  
  本文從初始需求開始構建聊天室模型以及對個案進行研究在不同的開發階段分別要用到UML類圖時序圖和狀態圖這樣難免需要確定一致性問題現在已經提出了許多仿真和方法用來確保模型各個方面的一致性我們關注內部一致性即給定模型內部制品之間的一致性問題
  
   簡介
  
  軟件系統的開發過程通常會被劃分成一些步驟每個步驟會用到不同的UML圖由於建模系統變得越來越復雜一致性問題就越發突出起來而在其中有兩種類型或問題更為顯著第一內部一致性問題涉及給定模型內部制品之間的一致性第二系統之間一致性問題涉及軟件開發過程中不同演化模型之間的一致性我們主要關注於內部一致性問題
  
  不同的文獻提出了不同的形式化方法用來自動檢查一致性發現設計當中存在的問題在下面幾節裡我們分步研究了一個聊天室的開發過程本文的靈感來源於Agder大學Geir Melby完成的一次項目報告()這個模型提出了一些潛在的一致性問題對於它們當中的部分內容也給出了自動化的一致性檢查方法
  
  在這份案例研究中我們從需求開始開發了一個聊天室模型第二節給出了客戶管理器對象以及聊天室之間的通信協議作為初始需求第三節研究了一個可能的類的設計它定義了符合協議的接口第四節中給出的時序圖進一步定義和描述了組件之間的通信並保持與類設計之間的一致性第五節使用狀態圖更進一步地確定應用程序的行為這份規程可以在我們的SVM(狀態圖虛擬機)環境中實時地進行仿真或執行在第六節中討論了協議規程與仿真跡的一致性第七節進行總結
  
   通信協議
  
  我們將要創建的聊天室程序是按照客戶機/服務器范型來架構的客戶會隨機連接聊天室如果某個聊天室接收了客戶客戶就會發送消息給這個聊天室然後聊天室廣播每條消息除了發送者以外每個與聊天室建立連接的客戶都會收到一份拷貝
  
  下面將要描述一個特定的簡化了的用例
  
  X     系統包括五個客戶和兩個聊天室客戶端最初沒有連接每隔一到三秒(非均勻分布)它們都會隨機連接一個聊天室被請求的聊天室同時收到請求(假定沒有網絡延時並且通信可靠)
  
  X     一個聊天室至多接收三個客戶當且僅當容量沒有超標時聊天室才會接收連接
  
  X     發出請求的客戶會立刻收到接收或拒絕通知
  
  X     在客戶可以發送聊天信息之前必須被一個聊天室接收
  
  X     連接建立之後客戶會每隔一到五秒(非均勻分布)給它所連接的聊天室發送隨機消息聊天室會立即接收消息它將耗時一秒鐘來處理接收到的消息並把它廣播給除發送者之外的所有連接客戶
  
  X     客戶會同時收到廣播為了簡化起見我們不討論沒有連接的情況
  
   類的設計
  
  根據上面的規定顯然我們需要兩個類Client和ChatRoom在開發過程早期階段對於仿真來說無需用戶干預我們明確地按照隨機過程對用戶行為(連接請求和聊天信息)進行建模以後客戶模型將會被與軟件打交道的真實客戶所代替仿真開始時會初始化五個Client實例和兩個ChatRoom實例
  
  我們還加入了一個singleton類ManagerManager以仲裁者的身份中繼組件之間的所有通信這種中央控制措施將會幫助截取系統傳遞的所有消息使用它們就可以檢查模型的正確性
  
  圖一描述了由這三個類組成的UML類圖
  
  X     ChatRoom提供兩個方法處理到達的事件request處理來到的請求每個請求都有參數clientID和roomIDChatRoom把接收或拒絕通知發回擁有全局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接收mrequestmaccept和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
  
  很容易就可以看出這些擴展並沒有增加狀態圖的表現力
  
   擴展狀態圖形式體系中的聊天室模型
  
  ClientChatRoom和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
    推薦文章
    Copyright © 2005-2013 電腦知識網 Computer Knowledge   All rights reserved.