沈曉奕 楊德仁

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

1 引言

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

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

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

2 CSP基本運(yùn)算定義

CSP 使用數(shù)學(xué)化符號(hào)來描述并發(fā)進(jìn)程的代數(shù)理論，CSP基本運(yùn)算符如下所示。

1）STOP 表示一個(gè)中斷的進(jìn)程，永遠(yuǎn)不會(huì)進(jìn)行任何的外部通訊，即不做任何事情的死鎖進(jìn)程。

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

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

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

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

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

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

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

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

3 UML活動(dòng)圖分析

3.1 UML活動(dòng)圖概述

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

3.2 UML活動(dòng)圖的元模型

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

圖1 活動(dòng)圖元模型

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

圖2 簡(jiǎn)單活動(dòng)模型

3.3 活動(dòng)圖的形式化定義

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

定義1活動(dòng)圖是一個(gè)三元組AD=（N，E，C），其中:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4.1 初始節(jié)點(diǎn)

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

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

圖3 初始節(jié)點(diǎn)

4.2 動(dòng)作節(jié)點(diǎn)

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

圖4 住院活動(dòng)示例

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

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

根據(jù)圖4 中簡(jiǎn)單的住院活動(dòng)示例，給出了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é)點(diǎn)

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

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

圖5 判斷節(jié)點(diǎn)

4.4 合并節(jié)點(diǎn)

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

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

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

圖6 合并節(jié)點(diǎn)

4.5 分叉節(jié)點(diǎn)

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

圖7 分叉節(jié)點(diǎn)

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

4.6 結(jié)合節(jié)點(diǎn)

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

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

圖8 結(jié)合節(jié)點(diǎn)

4.7 結(jié)束節(jié)點(diǎn)

結(jié)束節(jié)點(diǎn)包括活動(dòng)終止節(jié)點(diǎn)和流終止節(jié)點(diǎn)。活動(dòng)終止節(jié)點(diǎn)是指用來終止一個(gè)活動(dòng)的節(jié)點(diǎn)。在活動(dòng)中，可以有多個(gè)活動(dòng)終止節(jié)點(diǎn)，只要有一個(gè)控制流程到達(dá)活動(dòng)終止節(jié)點(diǎn)，該活動(dòng)的所以流程都會(huì)被全部終止。流終止節(jié)點(diǎn)是指用來終止活動(dòng)中的一個(gè)流?；顒?dòng)中可以存在多個(gè)流，并且當(dāng)流上的控制令牌達(dá)到流終止節(jié)點(diǎn)時(shí)，該流被終止?；顒?dòng)中一個(gè)流的終止不會(huì)影響活動(dòng)中其他流的執(zhí)行。因此，活動(dòng)終止節(jié)點(diǎn)和流終止節(jié)點(diǎn)分別映射到CSP 中的SKIP和STOP，如圖9所示。

圖9 活動(dòng)終止節(jié)點(diǎn)和流終止節(jié)點(diǎn)

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

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

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

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

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

基于圖10 中可中斷活動(dòng)區(qū)間的住院活動(dòng)圖，其轉(zhuǎn)換為CSP語(yǔ)言的描述如下:

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ù)過程作為一個(gè)案例研究，對(duì)嵌套的層次活動(dòng)圖進(jìn)行形式化描述，建立病人看病活動(dòng)圖以及復(fù)合活動(dòng)圖的子圖，即網(wǎng)上預(yù)約掛號(hào)，詳見圖11。

圖11 層次活動(dòng)圖

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

在病人看病活動(dòng)圖中，病人到醫(yī)院找醫(yī)生看病，醫(yī)生給病人下門診醫(yī)囑，醫(yī)生給病人下門診醫(yī)囑這一個(gè)過程可分為兩個(gè)并發(fā)執(zhí)行的流程:并發(fā)流一，醫(yī)生診斷后下達(dá)門診醫(yī)囑給病人開藥，否則病人健康，不需要藥物治療，流程結(jié)束；并發(fā)流二，醫(yī)生診斷后下達(dá)門診醫(yī)囑并為病人提供病人檢驗(yàn)、病理、超聲、醫(yī)學(xué)影像等基礎(chǔ)診斷治療服務(wù)，治療健康后離開醫(yī)院［21～23］。

接下來，我們使用CSP語(yǔ)言對(duì)嵌套的層次活動(dòng)圖作形式化描述，為了方便起見，分別對(duì)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é)語(yǔ)

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