一種利用CSP 轉(zhuǎn)換UML 活動圖模型的方法?

沈曉奕 楊德仁

（1.寧夏醫(yī)科大學公共衛(wèi)生與管理學院 銀川 750004）（2.寧夏醫(yī)科大學理學院 銀川 750004）

1 引言

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

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

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

2 CSP基本運算定義

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

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

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

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

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

5）P □ Q 表示外部選擇，執(zhí)行進程 P 或 Q 是由外部環(huán)境決定的。

6）P ∏Q 表示內(nèi)部選擇，內(nèi)部選擇轉(zhuǎn)換為分支選擇，外部環(huán)境不會影響選擇的方式。

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

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

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

3 UML活動圖分析

3.1 UML活動圖概述

UML 活動圖（Activity Diagrams，AD）由節(jié)點和邊組成，節(jié)點由動作或?qū)ο蟊硎?，邊是指動作之間的聯(lián)系。一個活動圖描述一個活動，通過對一個活動中的每個動作的關聯(lián)來表示活動的過程。UML活動圖可以分為兩種類型:基本活動圖和層次活動圖?；净顒訄D由基本元素組成，包括初始節(jié)點、動作節(jié)點、判斷節(jié)點、合并節(jié)點、分叉節(jié)點、合并節(jié)點、結(jié)束節(jié)點；層次活動圖表示一個嵌套活動圖，是指在一個活動圖中展示另外一個活動圖，活動狀態(tài)中的子圖顯示了活動圖的內(nèi)部結(jié)構(gòu)［16～18］。

3.2 UML活動圖的元模型

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

圖1 活動圖元模型

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

圖2 簡單活動模型

3.3 活動圖的形式化定義

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4 從AD到CSP的轉(zhuǎn)化及其規(guī)則

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

4.1 初始節(jié)點

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

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

圖3 初始節(jié)點

4.2 動作節(jié)點

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

圖4 住院活動示例

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

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

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

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 判斷節(jié)點

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

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

圖5 判斷節(jié)點

4.4 合并節(jié)點

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

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

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

圖6 合并節(jié)點

4.5 分叉節(jié)點

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

圖7 分叉節(jié)點

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

4.6 結(jié)合節(jié)點

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

規(guī)則6 結(jié)合節(jié)點:給定一個結(jié)合節(jié)點j，那么H（j）= χ（e）。

圖8 結(jié)合節(jié)點

4.7 結(jié)束節(jié)點

結(jié)束節(jié)點包括活動終止節(jié)點和流終止節(jié)點。活動終止節(jié)點是指用來終止一個活動的節(jié)點。在活動中，可以有多個活動終止節(jié)點，只要有一個控制流程到達活動終止節(jié)點，該活動的所以流程都會被全部終止。流終止節(jié)點是指用來終止活動中的一個流?；顒又锌梢源嬖诙鄠€流，并且當流上的控制令牌達到流終止節(jié)點時，該流被終止。活動中一個流的終止不會影響活動中其他流的執(zhí)行。因此，活動終止節(jié)點和流終止節(jié)點分別映射到CSP 中的SKIP和STOP，如圖9所示。

圖9 活動終止節(jié)點和流終止節(jié)點

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

4.8 可中斷活動區(qū)間

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

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

圖10 基于可中斷活動區(qū)間的住院活動圖

基于圖10 中可中斷活動區(qū)間的住院活動圖，其轉(zhuǎn)換為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”；如果 ? 特殊事件發(fā)生，B的值等于假；否則，B值為真。

5 案例研究

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

圖11 層次活動圖

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

在病人看病活動圖中，病人到醫(yī)院找醫(yī)生看病，醫(yī)生給病人下門診醫(yī)囑，醫(yī)生給病人下門診醫(yī)囑這一個過程可分為兩個并發(fā)執(zhí)行的流程:并發(fā)流一，醫(yī)生診斷后下達門診醫(yī)囑給病人開藥，否則病人健康，不需要藥物治療，流程結(jié)束；并發(fā)流二，醫(yī)生診斷后下達門診醫(yī)囑并為病人提供病人檢驗、病理、超聲、醫(yī)學影像等基礎診斷治療服務，治療健康后離開醫(yī)院［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 結(jié)語

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