一種利用CSP 轉換UML 活動圖模型的方法?

沈曉奕 楊德仁

（1.寧夏醫科大學公共衛生與管理學院 銀川 750004）（2.寧夏醫科大學理學院 銀川 750004）

1 引言

進程代數是一種一般性的形式化描述方法［1～2］，具有嚴格的理論依據、嚴謹的語義及其可擴展性。進程代數對并發、異步和非確定性事件的描述，適用于UML 活動圖模型中具有并發控制流的分叉節點、判斷節點和合并節點，代數分析步驟針對具體問題建立模型、特征描述與模型檢驗。通訊順序進程（Communicating Sequential Process，CSP）是著名計算機科學家C.A.R.Hoare在1978年提出的一種代數理論，用于描述過程中發生的事件與進程之間的關系，代數演算能力較為完整［3～5］。CSP規范了業務過程中的行為，并通過規則進行嚴格的數學推理，以形式化語言有效地描述和解釋業務過程模型。

國內外對活動圖模型的形式化方法展開了廣泛的研究，特別是在活動圖模型和CSP相結合的形式化表示中。文獻［6］使用UML 和CSP 捕獲相同的抽象級別即業務過程建模，用規則定義了從可視化過程模型UML 活動圖到可分析的代數模型CSP的映射。文獻［7～8］使用CSP 表示FUML 活動圖元素及其語義行為，將FUML 活動映射為可接受不同參數的父CSP進程，每個子過程在這個活動中充當不同的FUML元素。文獻［9］提出了一種改進UML行為圖的工作流建模方法，使用CSP語言描述活動圖模型并補充了活動圖模型的操作語言。文獻［10］提出了一種新的CSP指稱語義模型，即關鍵跡模型，并提出了模型的遞歸計算策略，論證了這種新的CSP 指稱語義模型驗證的可行性。文獻［11］使用CSP 的SysML 塊的形式化模型，提出了一種既包含狀態又包含活動的總體行為語義，并對這兩個構造的組合行為形式化描述。文獻［12～13］將活動圖的基本元素映射到Petri 網，實現了UML 活動圖的語法和語義形式化描述，但是這個過程需要將活動圖模型轉換為Petri 網模型，不能直接對活動圖模型進行形式化描述。由于UML 活動圖屬于半形式化語義并具有較高的復雜性，它的高級構造子，如可中斷活動區間和層次活動圖在實踐中很少使用。在UML 活動圖的語義域中有相關工作，如形式化定義UML 活動圖的節點，但是缺乏對活動圖的高級構造子的形式化研究［14］。

由于UML 活動圖是半形式化的模型，致使UML 活動圖不能直接推理和確切語義的缺失。為了確保UML 活動圖模型的正確性，需要我們選擇適合的形式化方法轉換UML 活動圖模型［15］。本文突破傳統的以狀態及其轉換為中心的Petri 網形式化表示方法，使用CSP 作為語義域，通過引入一組映射規則，采用了一種利用CSP 轉換UML 活動圖模型的方法，并以醫療領域為例進行實例分析，實現了活動圖模型的形式化描述與驗證。

2 CSP基本運算定義

CSP 使用數學化符號來描述并發進程的代數理論，CSP基本運算符如下所示。

1）STOP 表示一個中斷的進程，永遠不會進行任何的外部通訊，即不做任何事情的死鎖進程。

2）SKIP表示進程不做任何事情直到最后終止。

3）P||Q 表示進程間的同步并發，進程P 與進程Q中相同的事件同步執行。

4）B＆P 是一個被保護的表達式，其中B 指布爾表達式，因此，只有在B 為真時才會執行進程P，選擇操作表示為|。

5）P □ Q 表示外部選擇，執行進程 P 或 Q 是由外部環境決定的。

6）P ∏Q 表示內部選擇，內部選擇轉換為分支選擇，外部環境不會影響選擇的方式。

7）P；Q為進程間的順序組合，執行進程P，進程P成功終止后，執行進程Q。

8）P Δ Q 表示中斷，進程 P 在 Q 的第一個事件發生時中斷，P 永遠不再恢復。中斷條件不滿足，順序執行操作序列P，中斷條件滿足，執行操作序列Q。

9）?·P Δ（? →Q）是一種特殊的中斷事件，稱為特殊事件。

3 UML活動圖分析

3.1 UML活動圖概述

UML 活動圖（Activity Diagrams，AD）由節點和邊組成，節點由動作或對象表示，邊是指動作之間的聯系。一個活動圖描述一個活動，通過對一個活動中的每個動作的關聯來表示活動的過程。UML活動圖可以分為兩種類型:基本活動圖和層次活動圖。基本活動圖由基本元素組成，包括初始節點、動作節點、判斷節點、合并節點、分叉節點、合并節點、結束節點；層次活動圖表示一個嵌套活動圖，是指在一個活動圖中展示另外一個活動圖，活動狀態中的子圖顯示了活動圖的內部結構［16～18］。

3.2 UML活動圖的元模型

UML 活動圖元模型以UML 類圖的形式將建模語言的抽象語法形式化［19～20］。元模型的類捕獲語言的主要概念及其屬性。這些概念的相互關系通過關聯被捕獲。最后，將類安排到繼承層次結構中。UML活動圖的元模型如圖1所示。

圖1 活動圖元模型

圖2 顯示了一個簡單活動圖的示例，其中包含兩個活動邊，一條邊將一個初始節點與一個動作連接起來，一條邊將動作與一個結束節點連接起來。右邊的圖顯示了如何根據圖1 所示的元模型來表示這種具體的語法。

圖2 簡單活動模型

3.3 活動圖的形式化定義

為了方便描述活動圖的概念和基本信息，下面給出了活動圖的形式化定義。

定義1活動圖是一個三元組AD=（N，E，C），其中:

1）N=Na∪No∪Nc，N 是 UML活動圖的有限活動節點集合，Na為有限的動作節點集合；No是有限對象節點集合；Nc是一組有限的控制節點集合。

2）E=｛e| e 是活動圖的一條邊｝，E 是一組有向邊的有限集合。活動邊分為兩種類型:控制流（Control Flow）和對象流（Object Flow）。定義 E=Ec∪Eo，其中Ec是有限的控制流集合，Eo是有限的對象流集合。Ec和Eo是兩個不相交的集合，即Ec∩Eo=?。

3）C 表示包含在活動圖中的圖形元素，它的正式定義為如下所示的元組。C=（Activities，IR，EH，ER），其中Activities 是參數化行為的規格說明，行為被定義為下級單元的協調順序，其中下級單元的單個元素是動作；IR 是一組有限的可中斷活動區間；EH 是一組有限的異常處理器；ER 是一組有限的擴展域。

定義2將控制節點劃分為以下不相交集，表示為Nc=I∪D∪M∪F∪J∪T，其中:

1）I=｛i|i 是活動圖中的初始節點｝為初始節點的有限集合，一個活動可以有多個初始節點；

2）D=｛d|d是活動圖中的判斷節點｝是一組有限的決策，它們是在傳出流之間進行選擇的控制節點；

3）M=｛m|m 是活動圖中的合并節點｝是一組有限的合并集；

4）F=｛f|f 是活動圖中的分叉節點｝是一組有限的分叉流，將一個流分為多個并發的流；

5）J=｛j|j 是活動圖中的結合節點｝是一組有限的連接集；

6）T=｛t|t 是活動圖中的結束節點｝為結束節點的有限集合，包括活動結束節點和流結束節點；所以它可以表示為T=Ta∪Tf，其中Ta表示活動結束節點的有限集，Tf表示流結束節點的有限集。

定義3令Sin表示活動圖中一個節點的輸入邊，Sin（n）=｛e|e?E，e是n節點的輸入邊且n?N｝。

定義4令Sout表示活動圖中一個節點的輸出邊，Sout（n）=｛e|e?E，e是n節點的輸出邊且n?N｝。

定義5? e?E，n ?N，設n 是e 的目標，那么e和 n 之間的關系記為 Tar（e）=n。同理，設 n 是 e 的來源，則表示為Src（e）=n。

4 從AD到CSP的轉化及其規則

在從AD 到CSP 的映射被定義為一個函數HAD:n →CSP，n ?N∪C。在下面的小節中將推導出活動圖的CSP 描述。為簡單起見，一個新的運算符 χ如下定義。

4.1 初始節點

初始節點是控制節點，活動從初始節點啟動執行。初始節點沒有入邊，只有出邊，由實心小圓圈表示。如果n 是一個初始節點，那么|Sout（n）|=1 且|Sin（n）|=0，從初始節點到CSP 的映射規則如圖3 所示。

規則1 初始節點:給定一個初始節點n，且n ?I，如果e?Sout（n）?e?Ec，那么H（n）= χ（e）。

圖3 初始節點

4.2 動作節點

動作是行為規范的基本單元，表示活動中的單個步驟。下面定義從動作節點到CSP規范的映射。

圖4 住院活動示例

規則2 動作節點:給定一個動作節點n，且n ?Na，e ?Sout（n），如果|Sout（n）|=1，那么H（n）=n→χ（e），

否則H（n）=n→（e:Sout（n）→χ（e））。

根據圖4 中簡單的住院活動示例，給出了CSP代數理論的具體推理過程，如下所示。

HAD=H（i）

H（i）= χ（e1）

χ（e1）=H（“Please Hospitalization Procedure”）

H（“Please Hospitalization Procedure”）=Please Hospitalization Procedure→ χ（e2）

H（“Live In The Hospital”）=Live In The Hospital

∴ HAD=Please Hospitalization Procedure→Fulfilled→Live In The Hospital

4.3 判斷節點

判斷節點是在活動中實現多流判斷的控制節點。判斷節點具有一條入邊和多條出邊，由菱形框表示，如圖5所示。

規則3 判斷節點:給定一個判斷節點n，且n ?D，e ?Sout（n），因此|Sout（n）|＞1 ?|Sin（n）|=1，那么H（n）=n→（e:Sout（n）→χ（e））。

圖5 判斷節點

4.4 合并節點

合并節點將多股有條件的進入控制流合并成為一股控制流，如圖6所示。因此，CSP中合并節點的形式化如下所示。

規則4 合并節點:給定一個合并節點n ?M，e?Sout（n），因此|Sout（n）=1|，那么H（n）= χ（e）。

馬克思主義與馬克思主義大眾化研究學科是“源”與“流”的關系。從學科維度考量，馬克思主義大眾化研究學科是馬克思主義學科發展所驅，馬克思主義的實踐性、社會性、歷史性與主體性等特征，決定馬克思主義必然大眾化。從政治維度考量，馬克思主義的階級屬性與理論使命，也決定馬克思主義必然大眾化。因此，馬克思主義大眾化研究學科的建設與發展，必受到真理性與價值性的促進或制約，真理性體現學術發展的需要，價值性則體現鞏固意識形態的需要。馬克思主義大眾化研究學科的真理性與政治性特征，決定了馬克思主義大眾化研究學科必須要以馬克思主義作為根本支撐，同時還必須要借助其他學科作為重要支撐。

圖6 合并節點

4.5 分叉節點

分叉是生成并發控制流的有效機制，分叉節點屬于控制節點，有一個入邊和多條出邊，分叉在活動中把一個流分為多個并發流。因此，分叉是生成并發控制流的有效機制。分叉用一條棒表示，如圖7所示。

圖7 分叉節點

規則5 分叉節點:給定一個分叉節點n ?F，e ?Sout（n），因此|Sout（n）|＞1，那么H（n）=|| e:Sout（n）·χ（e）。

4.6 結合節點

結合節點是與分叉完全相反的控制節點，有多個入邊和一個出邊，其作用是把活動圖中的多股流匯合成一股流，以實現多個流的同步機制，如圖8所示。

規則6 結合節點:給定一個結合節點j，那么H（j）= χ（e）。

圖8 結合節點

4.7 結束節點

結束節點包括活動終止節點和流終止節點。活動終止節點是指用來終止一個活動的節點。在活動中，可以有多個活動終止節點，只要有一個控制流程到達活動終止節點，該活動的所以流程都會被全部終止。流終止節點是指用來終止活動中的一個流。活動中可以存在多個流，并且當流上的控制令牌達到流終止節點時，該流被終止。活動中一個流的終止不會影響活動中其他流的執行。因此，活動終止節點和流終止節點分別映射到CSP 中的SKIP和STOP，如圖9所示。

圖9 活動終止節點和流終止節點

規則7 結束節點:給定一個節點n?T，如果n?Ta，那么 H（n）=SKIP，否則，如果 n ? Tf，那么H（n）=STOP。

4.8 可中斷活動區間

可中斷活動區間是活動圖中的特殊活動區域，包括多個活動節點和活動邊，當外部引發的一個或多個特殊事件在該區域內發生時，必須通過中斷邊將特殊事件連接到區域外的一個活動節點。該區域在執行動作的過程中，如果發生特殊事件，那么終止該區域中的所有活動，轉去執行外部特殊事件并將控制傳遞給中斷邊連接的外部節點。

規則8 可中斷活動區間:設e 是可中斷活動區間中的中斷邊，n ?IR，P 是代表可中斷活動區間中活動的過程，那么H（n）=P Δ (? → H(T ar( e )))；（B＆χ（e?）），? 表示中斷事件的發生，B 是一個布爾表達式。如果? 特殊事件發生，那么B 是假的，則執行Q；否則B為真，則執行P。e?是非中斷活動區間的邊，它的源節點在區域內，目標節點在區域外。

圖10 基于可中斷活動區間的住院活動圖

基于圖10 中可中斷活動區間的住院活動圖，其轉換為CSP語言的描述如下:

HAD=Please Hospitalization Procedure

→Live In The Hospital

→（（Receive Treatment || Receipt Of Bill→Make Payment→Accept Payment）→SKIP）

Δ（ ? →Cancel Hospitalization→SKIP）；（B＆Leave The Hospital→SKIP）

? 表示接受事件“Patient Died”；如果 ? 特殊事件發生，B的值等于假；否則，B值為真。

5 案例研究

在此部分，我們以某共享醫院業務過程作為一個案例研究，對嵌套的層次活動圖進行形式化描述，建立病人看病活動圖以及復合活動圖的子圖，即網上預約掛號，詳見圖11。

圖11 層次活動圖

在子圖網上預約掛號中，用戶通過登錄官方微信服務號或APP等渠道預約掛號，選擇相應專業的醫生或科室，確認并提交訂單。系統接收訂單則確認購買掛號單，訂單完成，否則顯示暫未綁定或新建就診卡信息，系統拒絕訂單，病人完善信息后需要重新提交訂單。

在病人看病活動圖中，病人到醫院找醫生看病，醫生給病人下門診醫囑，醫生給病人下門診醫囑這一個過程可分為兩個并發執行的流程:并發流一，醫生診斷后下達門診醫囑給病人開藥，否則病人健康，不需要藥物治療，流程結束；并發流二，醫生診斷后下達門診醫囑并為病人提供病人檢驗、病理、超聲、醫學影像等基礎診斷治療服務，治療健康后離開醫院［21～23］。

接下來，我們使用CSP語言對嵌套的層次活動圖作形式化描述，為了方便起見，分別對User Logs In，Appointment Registration，Choose A Doctor，Commit Order，Patient ID Card Problem，Complete Information，Confirm Purchase，Order Complete，See A Doctor，Diagnose，Treatment Of Diseases，Prescribe drugs，Leave The Hospital 采用其首字母縮寫代替，即分別表示為 ULI，AR，CAD，CO，PICP，CI，CP，OC，SAD，D，TOD，PD，LTH。其過程如下:

HAD=ULI→AR→CAD→CO

→（Order Rejected→PICP →CI|Order Accepted→CP）

→OC →A.SAD →B.D

→B.（（（True）＆PD|（False）＆STOP））||B.TOD）

→A.LTH

→SKIP

6 結語

本文采用了一種利用CSP 轉換UML 活動圖模型的方法。首先，簡要的介紹了CSP 語言，對UML活動圖進行了分析，并給出活動圖形式化定義。接下來，通過活動圖的節點和可中斷活動區間說明了活動圖模型到CSP 的映射規則。最后以某共享醫院業務流程為案例研究，驗證CSP代數理論對層次活動圖模型等高級構造的數學推理和形式化表示。本文所做的工作目前已經涵蓋了活動圖的初始節點、動作節點、判斷節點、合并節點、分叉節點、合并節點、結束節點、可中斷活動區間和嵌套的層次活動圖模型等的形式化。由于空間的限制，對部分活動圖模型概念和符號形式化描述暫未介紹，如數據流和對象流等，未來進一步工作是完善活動圖模型到CSP轉化規則，以滿足活動圖模型更多特性。