一种工作流形式化建模方法

不能很好的支持，尤其是缺乏对工作流模式进行形式化描述的方法.本文提出了一种新的选 择逻辑，和传统的数理逻辑相比，针对工作流建模进行了优化，具有更加简单、易于理解 的形式；使用选择逻辑建模时，将工作流模式拆分为汇合逻辑和分支逻辑，不仅能形式化

地描述工作流模式，并且能够进一步表达工作流模型中与业务元素有关的要素，从而可以 很好地支持业务过程建模.关键词过程逻辑；工作流模式；业务过程建模；逻辑规则中图分类号TP3U

文献标识码A0引言在工作流模式中，文献［1］通过抽象多个组织中的实际业务需求，总结了 20种常见

的工作流模式.对工作流模式的支持，代表了工作流管理系统在控制流方面的表达能力.

现有的形式化建模方法对基本的工作流模式大多可以进行形式化地描述，但对一些复杂

的工作流模式进行形式化描述时存在有歧义、无法写出文法规则、不利于解释实现的问

题，因此现有的工作流系统对一些复杂的工作流模式尚不能很好地支持.UML AD3］和

EPQT能直观地表示业务流程，但它们是图形化的建模方式，缺少严格的语义定义. Petr^冋网适合建模基于状态的工作流模式，但对一些高级模式，Petri网显得力不从心. YAWL®］提出基于卩点说网的新的建模语言YAML, SNP^利用尖峰神经P系统对20种 工作流模式建模，但它们的实际应用效果还需要进一步验证• Pi-演算卩坷是一种进程代

数，具有严格的数学基础，可以用于业务流程的建模•本文提出了一种形式化的工作流建模方法，并选取了部分工作流模式为例，给出了 具体的表达方式，最后以一个业务过程的建模实例验证了该方法的可行性.收稿日期：2019 - 04 - 03作者简介：李 新（1974-）,男（汉族），四川省成都市人，博士/副教授，研究方向：工作流、机器学习.E-mail: lixin@ stu.edu.cn34汕头大学学报(自然科学版)第35卷1选择逻辑数理逻辑可以用全称量词、存在量词和相等性描述数量概念.例如，\"不多于两个学生\"这句话可以表示为：\\x,y,z：student*x = yvy = zvz = x而\"至少有两个学生\"可以表示为，3x,y:student*x^y“恰好有一个”的概念则需要同时借助全称量词、存在量词以及相等性•例如，“恰好

有一个学生参加活动”可以表示为，. student• p/Ny: student*p[ylx\\~^y = x从上面的描述可以看出,当要表达“不超过10个”、“至少10个”或者“n个中恰好有

5个”这样的概念时，用数理逻辑去描述，表达方式将会非常冗长并且难以看懂.从以往 的经验中可以看出，这一点明显妨碍了数理逻辑在工作流形式化描述领域的应用.为了对工作流模式进行更好的形式化描述，本文提出了一种新的选择逻辑 (SelectLogic),其基本形式如下，SelectLogic^Set ,m,n)表示在一个Set中可以选择出number个元素(mWnumberWn)时，SelectLogic^Set, ffi,\")取值为真.当 m = n 时，SelectLogic(list,m,m)简写为 SelectLogic(list,m).选择逻辑涵盖了基本的数理逻辑运算和数量表达功能,能够方便地应用于工作流的 形式化描述领域•下边是基本逻辑运算在选择逻辑中的表达形式，1. 与运算A AB,对应的 SelectLogic 表达式为，SelectLogic({A,B},2).2. 或运算AVB,对应的 SelectLogic 表达式为，SelectLogic([A,B}, 1,2).3. 异或运算(-.AAB) V(--BAA),对应的 SelectLogic 表达式为，SelectLogic(.{A,B],l')-4. 非运算-■A,对应的 SelectLogic 表达式为，SelectLogic^ {not A}, 1).选择逻辑能够表达斟的逻辑运算，而15寸于复杂的运算也能以简单的形式标如下・5. 数量选择，”恰好有n个”数理逻辑表达形式见前文，需要引入量词的形式，而对应的SelectLogic表达式为, SelectLogic^list, 5),形式简单得多.6. 数量选择，\"至少m个，不超过n个\"数理逻辑需要组合全称量词、存在量词和相等性等概念，表达形式显得繁琐和冗

长，在此略过.而对应的SelectLogic表达式为，SelectLogic^list综上所述，选择逻辑(SelectLogic)相对于数理逻辑，其形式更加简单，且易于理解,

因此，更适合应用在工作流建模的环境中.2工作流模式的形式化表示方法工作流模式是经常在业务流程建模中使用的重复出现的问题的解决方案，从控制流

第1期刘宇等：一种工作流形式化建模方法35的角度系统地描述了过程定义语言需要满足的业务需求，与特定的工作流语言无关•下 图是两种常见的工作流模式：顺序模式和并行分支模式(见图1),这两种模式表示当前

一个活动状态为完成时，后一个或者后一组活动可以开始启动.图1两种工作流模式示意图现有的工作流技术把工作流模式作为工作流建模的基本构造单元，但其实，过程逻

辑可以被划分为更小的单元，如图2所示.图2过程逻辑分解示意图图中存在两组活动集，活动集]经过某种逻辑进行汇合，又经过分支逻辑将流程转 移到活动集2.汇合逻辑和分支逻辑的组合即是过去被看作一个整体单元的工作流模式.

汇合逻辑和分支逻辑的内容有所不同，汇合逻辑中的内容是活动的状态，而分支逻辑中

的内容是活动的动作•这样做的好处是可以对过程逻辑的性质进行更细致的分析，以便 对过程逻辑进行更好的抽象•一个工作流模式即可表示为，汇合逻辑- > 分支逻辑.下边对常见的一些工作流模式运用选择逻辑进行形式化描述，1顺序模式顺序逻辑是最简单的过程逻辑形态，它表示在流程中，只有前一个任务执行完毕

T ,后一个任务才能开始执行•其流程图如图la中所示.选择逻辑的表达形式为：SelectLogic([A}, 1}) - > SelectLogic( {B}, 1}).2并行模式并行模式表示在流程中，需将单进程的某控制点分成可并行执行的多进程控制，于 是允许任务同时执行或以任何顺序执行•其流程图如图lb中所示.选择逻辑的表达形式为：SelectLogic^{A}, 1}) - > SelectLogic^{B,C\\, 2}).3同步模式同步模式表示在流程中的某个点，有多个并行的子流程或者任务合并成一个流程. “同步”指这个流程必须等待所有的分支都执行完成后，才能激活后面的任务•其流程图

如图3所示，36汕头大学学报(自然科学版)第35卷图3同步模式选择逻辑的表达形式为：SelectLogic{{A, B}, 2})->SelectLogic({C}, 1}).4独占式选择模式独占式选择模式表示当一个任务完成后，可以有多个分支进行选择，但是只能选择 其中一个分支，其他的分支将不会进行下去，即多选一.其流程图如图4所示：图4独占式选择模式选择逻辑的表达形式为：SelectLogic^{A}, 1})- > SelectLogici.{B, C, D}, 1}).5简单合并模式简单聚合模式表示多个可以选择的分支在某一点合并成一个分支，但是只有一个分 支可以被接受，遵循先到先得的原则•其流程图如图5所示:图5简单合并模式

选择逻辑的表达形式为：SelectLogic^[A, B, C}, 1})- > SelectLogic^.[B, C, D},1}).6多重选择模式多重选择模式表示当一个任务完成后，有多个分支进行选择，可以选择其中的一个

或多个分支•其流程图如图6所示:第1期刘宇等：一种工作流形式化建模方法37图6多重选择模式选择逻辑的表达形式为：SelectLogic({A}, 1}) - > SelectLogic(\\B,C}, 1, 2}).通过引入适当的系统函数对选择逻辑加以扩展，还可以形式化的描述更多、更复杂

的工作流模式，带有系统函数的选择逻辑大致形式为：SelectLogic(list, m, n, sysfunc*).其中，*表示0个或多个.3选择逻辑的文法文法是语言结构的描述工具，定义句型的结构，能够用有限的规则把语言的无限句

子集合描述出来•下边是选择逻辑文法规则(因篇幅所限只列出部分内容)，由于文法符 号较多，用符号A、B、C不易理解、容易产生混乱，因此采用文字加下划线的方法表

示文法符号.选择逻辑规则- > 汇合SelectLoxic表达式\"- > \"分支SelectLo^ic表达式汇合SelectLoxic表达式-> SelectLogic(状态表达式集合,整数数值,整数数值)状态表达式集合-> {状态表达式B}B-> ,状态表达式Bl\"状态表达式- > 比较表达式|汇合SelectSic表达式|逻辑变量|逻辑常数I not比较表达式| not逻辑变量| not逻辑常数比较表达式-> 属性 比较算符属性或数值属性或数值-> 属性〔数值属性- > 过程或活动•属性名称过程或活动- > 过程名称|活动名称过程名称-> 标识符活动名称- > 标识符属性名称-> 标识符数值_ >整数数值I小数数值I字符串整数数值- > 整数number小数数值-> 小数number字符串- > 字符串 number分支逻辑的逻辑结构和汇合逻辑是类似的，不同的是汇合逻辑表示的是活动的状

态，分支逻辑表示的是活动的动作•因此在文法规则里，分支逻辑用“动作集合”代替汇

合逻辑中的“状态表达式集合”.38汕头大学学报（自然科学版）第35卷值得注意的是，虽然汇合逻辑和分支逻辑的宏观文法结构类似，但是“状态”和

“动作”的文法结构却完全不同，尤其是，两者的语义处理大相径庭•因此，从文法结 构清晰和未来语义处理易于实现的角度，Selectlogic文法中没有将汇合逻辑和分支逻辑

合并表示而是分别表示，分开处理.定义了规则文法之后，即可根据文法规则写出规则解释器，并进而构建工作流引

擎，在此由于篇幅限制，以上内容省略•4业务建模实例假如银行小额贷款金额最高为V,则银行的贷款审批流程如下：1.客户提出贷款申

请；2•如果是小额贷款（贷款金额Wv）,由银行业务员对客户进行信用审核；如果信用 审核通过，则贷款申请通过；如果信用审核不通过，则贷款申请不通过；3.如果是大额 贷款（贷款金额〉v）,由银行业务员对客户同时进行信用审核和资产审核；若信用审核和

资产审核都通过，则贷款申请通过；若信用审核或资产审核未通过，则贷款申请不通过•使用工作流模式对贷款审批流程建模,示意图如图7所示:独占选择模式并行模式 同步模式图7贷款审批过程示意图其中，由于大额贷款审核时有两个并行的审核活动，为了满足工作流模式，需要添

加一个分支活动使审核活动分为信用审核和资产审核，还需要添加一个汇聚活动使两个 审核活动汇合•在对图7中的工作流模式进行实现时，许多工作流平台会要求用户编写

特定的程序代码，例如，按照贷款金额大小区分贷款审核途径等涉及业务数据的环节, 可能需要通过程序代码来实现.采用选择逻辑表达式建模，示意图如图8所示，流程如下•规则群1

/信用审核、\\^ 规则群2通过贷款申请\\、/尹\\资产审核不通过规则与规则群定义图8贷款审批过程结构示意图第1期1. 状态定义：刘宇等：一种工作流形式化建模方法39申请贷款金额：ActApply.money信用审核状态:ActCreditAudit. state资产审核状态：ActAssetsAudit. state2. 规则与规则群的定义：用于表达活动间过程逻辑的一条或多条规则构成一个规则群，规则群］包含两条规则：规则1一小额贷款申请：SelectLogic({Actapply.moneyWv}, 1)- >

SelectLogic({ActCreditAudit. start()}, 1)其中，Actapply表示贷款申请活动，ActApply.money表示贷款金额；ActCreditAudit 表示信用审核活动.规则2—大额贷款申请：SelectLogic({Actapply.money > v}, 1)- >

SelectLogic({ActCreditAudit.start( ), ActAssetsAudit.start()}, 2)其中，ActAssetsAudit表示资产审核活动.规则群2中包含三条规则:规则1—小额贷款审核通过：SelectLogic({Actapply.moneyWv, ActCreditAudit.state 二pass}, 2)- >SelectLogic ({ActApplyPass. start()}, 1)其中，ActApplyPass表示贷款审核通过活动.规则2—大额贷款审核通过：SelectLogic ({Actapply. money > v, ActCreditAudit. state = pass,ActAssetsAudit.state = pass}, 3)- > SelectLogic({ActApplyPass.start()}, 1) 规则3—审核不通过：SelectLogic ({ActCreditAudit. state 二 reject,ActAssetsAudi仁state=reject}, 1, 2)- >

SelectLogic({ActApplyNotPass. start()}, 1)其中，ActApplyNotPass表示贷款审核不通过活动.和图7相比，可以看到运用选择逻辑所建立的业务过程模型得到了明显的简化，活 动数量大为减少，并且不需要用户编写任何程序代码，过程逻辑和业务逻辑两者均统一 在逻辑规则这种形式化表示方法中.5结束语本文利用选择逻辑对工作流模式进行了描述，这种方法是完全形式化的，有效消除 了自然语言和图形中可能存在的歧义.相比传统的数理逻辑，本文提出的选择逻辑极大

地简化了过程建模的形式•同时，这种形式化方法可以直接写出对应的文法结构，这对 于工作流引擎的实现具有重要意义.目前工作流领域其它的形式化方法尚未见到和文法

40汕头大学学报（自然科学版）第35卷结构相关联的文献资料，意味着其它的形式化方法没有提及如何把形式化表示方法和工

作流引擎的技术实现联系起来.本文在这方面进行了开拓性的探索•通过文中的业务建 模实例验证了选择逻辑的建模能力和所具有的灵活性.下一步将着重研究复杂工作流模 式的形式化表示方法.参考文献[1] AALSTW, HOFSTEDE A, KIEPUSZEWSKIB. Workflow pattems[J]. Distributed and Parallel Databases,

2003, 14(1)： 5-51.[2] RUSSELL N, AALST W, HOFSTEDE A. On the suitability of UML 2.0 activity diagrams for business

process modelling[C]//Conceptual Modelling 2006, Third Asia-Pacific Conference on Conceptual Modelling

(APCCM 2005), Hobart, Tasmania, Australia, January 16-19 2006. DBLP, 2006.⑶ 马云龙，孙精科•基于UML的工作流建模的研究与分析[J].信息技术，2015(5)： 114-116.[4] AALST W. Formalization and verification of event-driven process chains [J]. Information and Software

Technology, 1999, 41(10)： 639-650.[5] JO§T G, HUBER J, HERItKO M, et al. An empirical investigation of intuitive understandability of

process diagrams [J]. Computer Standards & Interfaces, 2016, 48： 90-111.[6] HOFSTEDE A, AALST W. Workflow patterns: on the expressive power of (petri-net-based) workflow

languages[C]//Jensen(Ed.) Fourth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the

CPN Tools, 2002, 14(1)： 1-20.[7] KHELDOUN A, BARKAOUI K, IOUALALEN M. Fonnal verification of complex business processes

based on high-level Petri nets卩].Information Sciences, 2017, 385/386: 39-54.[8] 王斌，章云，王晓红.基于Petri网的工作流模式建模及应用[几计算机工程与应用，2008, 44

(13)： 238-241.[9] AALST W, HOFSTEDE A. YAWL： Yet another workflow language[J], Information Systems, 2004, 30

(4)： 245-275.[10] SONG T, ZENG X, ZHENG P, et al. A parallel workflow pattern modeling using spiking neural p

systems with colored spikes [J]. IEEE Transactions on Nanobioscience, 2018, 17(4): 474-484.[11] 黄贤明.工作流模式的兀演算建模研究[J].计算机工程与应用.2006, 43(17)： 66-68.[12] KHALED A, MILLER J. Using 兀-calculus for formal modeling and verification of ws-cdl choreographies

卩].IEEE Transactions on Services Computing, 2017, 10(2)： 316-327.[13] BOUSSETOUA R, BENNOUI H, CHAOUI A, et al. An automatic approach to transform BPMN

models to Pi-Calculus [C]//acs/ieee international conference on computer systems and applications,

2015： 1-8.（下转第53页）第1期时统业等：Hermite-Hadamard不等式差值估计的一种推广53[10] 时统业，徐建忠.几个涉及一阶导函数的(a,m)-凸函数的积分不等式[J].湖南理工学院学报(自然

科学版)，2018, 31(3)： 1-6.[11] 时统业.涉及可微(a,m)凸函数的单调函数和Hermite-Hadamard型不等式[J].广东第二师范学院

学报，2018, 38(3)： 32-37.[12] DRAGOMIR S S, CHO Y J, KIM S S. Inequalities of Hadamard*s type for Lipschitzian mappings and

their applications [J]. Journal of Mathematical Analysis and Applications, 2000, 245(2)： 489-501.[13] YANG G S, TSENG K L. Inequalities of Hadamard's type for Lipschitzian mappings [J]. Journal of

Mathematical Analysis and Applications, 2001, 260( 1): 230-238.[14] 任崇勋.Lipschitz函数的Hadamard型不等式[J].琼州大学学报，2006, 13(2)： 1-2 + 5.[15] 刘三阳，李广民.数学分析十讲[M].北京：科学出版社，2011： 72.A Generalization of Difference Estimation of

Hermite-Hadamard InequalitySHI Tongye1, ZENG Zhihong2(1. PLA Naval Command College, Nanjing 211800, Jiangsu, China;2. Editorial Department, Journal of Guangdong University o£ Education, Guangzhou 510303, Guangdong, China)Abstract In this paper, the function 0(x) = [

J a

J a+b-c一(兀一 a)[f(x) + b-x)].is considered. By using the identity, differential mean value theorem, the definition and property

of convex functions, estimates of this function are obtained in the case ofsatisfying M-Lipschiz condition, f bounded, and \\f \\ being convex function, respectively.Keywords convex function; differential function; Hermite-Hadamard type inequality; M-Lipschiz

condition(上接第40页)A Formal Modeling Method for WorkflowLIU Yu, LI Xin(College of Engineering, Shantou University, Shantou 515063, Guangdong, China)Abstract Workflow patterns define the basic structural characteristics of business process in workflow system. The support of workflow patterns is an import criterion to measure the expressive ability and applicability of workflow products in control flow. Many complex workflow patterns are

not well supported by current workflow products, especially the lack of formal description of

workflow patterns. A new selection logic is proposed, which is optimized for workflow modeling compared with traditional mathematical logic. When modeling with selection logic, the workflow

pattern is divided into merge logic and branch logic, which not only can describe the workflow pattern formally, but also further express the elements related to nosiness elements in the workflow model. Thus, the creation of the process can be well supported.Keywords process logic; workflow pattern; business process modeling; logic rule grammar analysis