一种利用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转化规则，以满足活动图模型更多特性。