结合Petri网与进程代数的业务过程协同模型研究

笪建+程耀坤+莫启

摘要：业务过程协同允许组织之间彼此进行通信、交互与协作以完成特定业务目标。为了完整地描述出一个参与组织的协同，提出进程标号迁移系统PLTS（Process Labeled Transition System），对单个参与组织的模型视图和通信行为视图序列进行集成，进而使整个跨组织业务过程协同可以通过各个参与组织的PLTS并行组合而成。该建模方法充分结合了Petri网与CCS各自的优势，避免了单一运用Petri网与进程代数建模业务过程时面临的问题，有效支持了业务过程协同的形式验证。同时为了避免模型状态空间过大而无法进行有效验证的问题，提出了6条约简规则，并证明了这些规则是满足协同正确性的充分条件，从而使行为验证方式由模型推导变为代数推导。

关键词：

Petri网；进程代数；跨组织业务过程； 进程标号迁移系统； 约简

DOIDOI：10.11907/rjdk.172661

中图分类号：TP301

文献标识码：A 文章编号：1672-7800（2017）012-0049-04

Abstract：Business processes collaboration enable organizations to communication， interact and cooperate with each other to achieve their business goals. To the whole cross-organization business process collaboration can be composed of the PLTS of every organization， this method combines the advantages of both Petri Net and CCS， avoiding the issues which occurs by applying petri net and process algebra respectively， which can effectively support collaboration business process formal verification， at the same time， to avoid the state space too big to verify， six rules is proposed and prove that the six rules can guarantee collaboration correctness， so that the mode of behavior verification from the model-based reasoning to algebraic reasoning.

Key Words：Petri Net；process algebra；cross-organization business； process labeled transaction system； reduction

0 引言

随着经济全球化与企业信息化的发展，企业经营模式也发生了很大变化，各个企业的业务活动已从独立模式发展为跨企业多目标合作的协同模式[1]。在现代环境下，没有一个企业是孤立存在的，企业仅作为参与者参与到业务协作中。在协作过程中，它们彼此交互，完成一定的业务功能[2]。一个业务过程是指用来规划企业的业务元素。在不同的组织业务过程中，通常会联系多个业务过程单元，组织边界被跨越，在电子商务环境下的跨组织信息系统中，业务功能和制造活动之间的流关系得到了广泛关注[3]。

1 相关研究

对于业务过程，研究者们提出了很多建模与分析方法。如文献[4]提出了严格的语义形式化方法，它的优点是能够精确地描述和分析业务过程，Petri网与进程代数主要关注了建模和分析业务过程协同；文献[5]提出，Petri网是一种比较好的业务过程建模语言，因为Petri网有直观的图形化表示、严格的形式语义、形式化的分析技术，可以清晰描述实例的控制流执行状态，可用跨组织业务过程建模；文献[6]提出，进程代数是一种很好的描述和分析并发系统的模型，进程代数具有的显式交互机制及组合特性最适合对通信、交互特征的跨组织业务过程进行建模，可以采用其中的归约表示由进程间相互作用形成的动态演化。

在业务过程协同方面， 文献[7]提出利用Petri网与进程代数进行建模与分析业务过程协同，得到了学术和工业界的广泛关注。在跨组织业务过程协同领域，对业务过程协同模型进行约简的文献并不多见。在文献[8]中，为了解决动态跨组织工作流协同问题，提出一种基于视图的方法对跨组织业务过程进行建模，并针对模型中的顺序结构、选择结构及并行结构提出了约简方法；文献[9]结合跨组织工作流建模与对象网之间的相似性，提出一种基于公共视图与对象Petri网的建模方法，并假定该网是自由选择网的基础，提出几种简单的约简方法；文献[10]针对跨组织应急联动系统的特性，在Petri网模型基础上进行扩展，提出了OTRM-Net，用于建模任务协同模式和应急处置流程，并对模型的约简进行了简单讨论。

综上分析，针对模型约简存在的主要问题，本文提出进程标号迁移系统，对单个参与组织的模型视图和通信行为视图序列进行集成，进而使整个跨组织业务过程协同可以通过各个参与组织的进程标号迁移系统并行组合而成。同时为了避免模型的状态空间过大而无法验证的问题以及减少验证代价，在考虑通信异步的基础上提出了6条约简规则，并证明这些规则是满足协同正确性的充分条件，从而将业务过程的验证由模型推导转变为代数推导。

2 进程标号迁移系统及约简

2.1 進程标号迁移系统

基于Petri网与CCS分别对业务过程模型视图和通信行为视图进行建模。对于一个模型视图，存在一个通信行为视图序列与之对应，该通信行为视图序列受模型视图内部状态的约束。为了完整描述出一个参与组织的协同，本文借鉴进程代数中标号迁移系统LTS（Labeled Transition System）的思想，引入进程标号迁移系统PLTS（Process Labeled Transition System），对单个参与组织的模型视图和通信行为视图序列进行集成。

定义1（进程标号迁移系统） BPV=（IV，PV，ftp）为一个业务过程模型视图，其进程标号迁移系统形式化定义为一个四元组PLTS=（R（M0），E，P，φ），其中：

（1）R（M0）是模型视图的可达状态集，称为顶点集；M0是模型视图的初始状态，称为根节点。

从定义1可以看出，进程标号迁移系统与标号迁移系统的区别在于：在LTS中，状态用进程表示，而在PLTS中，状态用内部视图中的标识表示；在LTS中，迁移关系用动作表示，而在PLTS中，迁移用通信行为进程和τ表示。

通过PLTS，可以完整地描述出单个参与组织的协同，进而使整个跨组织业务过程协同可以通过各个参与组织的PLTS＼+0并行组合而成。其中，PLTS＼+0表示某个模型视图初始状态所生成的进程标号迁移系统。

2.2 约简规则

模型建立的目的是为了更加准确、直观、自然地描述所要分析的系统，而验证则是以建立的模型为基础对系统进行定性和定量分析，以判断系统是否满足既定目标，以对其进行改进。对于跨组织业务过程协同中的某类复杂系统（如联合制造、供应链及电子商务等），其中单个参与组织内部的结构及所实现的业务逻辑复杂难懂，组织之间的交互关系错综复杂，跨组织业务过程协同的直接组合往往会使模型的状态空间过大而无法快速实现对该类复杂系统的验证。

在跨组织业务过程协同过程中，如果业务过程模型内部视图不能够正确终止，则协同必然会失败。因此，在本文中假定参与协同的业务过程内部视图都满足文献[7]中定义的合理性，并用合理性定义业务过程的正确性，进而使跨组织业务过程协同的验证变为组织之间交互关系的验证，即进程标号迁移系统之间交互关系的验证。

文献[8]中的研究结果表明，在协同过程中，一个参与组织的内部结构所拥有的弧集及状态集远远大于组织用于协同而开放的接口数，对这些弧集和状态集进行约简，能够极大地减少复杂系统的验证代价，提高验证效率。

综上述，约简规则应以进程标号迁移为基础，结合异步消息通信对模型视图中所拥有的弧集及状态集进行化简，只保留体现交互行为的通信行为视图及必要的内部行为，以达到减少模型状态空间的目的。由于在PLTS中只存在3种基本类型的结构：顺序、选择及循环，因而约简规则也从这3方面进行定义。

定义2（协同正确性） 对于参与协同的每一个业务过程，在给定初始标识的情况下，通过交互，使每一个业务过程都能正确结束，即满足合理性。

定义3（约简规则） 对于跨组织业务过程模型内部视图中的任意两个变迁t＼+1，t＼+2，t＼+1＼+·∩＼+·t＼+2=P，则约简t＼+1和t＼+2为t后满足：＼+·t=＼+·t＼+1+＼+·t＼+2-P，t＼+·=t＼+＼{1·＼}+t＼+＼{2·＼}-P。

约简规则1：令α为某个通信变迁所生成的通信行为视图，τ为某个瞬时变迁对应的行为，则τ；α可以约简为α，记为τ；α≈α。其中；表示两个进程的顺序执行，≈表示协同正确性互模拟。

证明：不妨设τ映射的瞬时变迁为a，进程α所映射的通信变迁为t。根据条件可知，约简后只存在通信变迁为t。根据约简前满足协同正确性及定义1可知，瞬时变迁a能够被执行，则＼+·a都有Token；又因为瞬时变迁a和通信变迁t是顺序执行，并满足瞬时变迁a执行之后通信变迁t能够执行，可知在执行瞬时变迁a后＼+·t都有Token。因为是顺序执行，设瞬时变迁a和通信变迁t之间的库所集为P，根据定义3可知，约简后＼+·t＼+＼{post＼}=＼+·a+＼+·t-P。分两种情况进行讨论：

（1）如果P=，则可以推出合并后运行到该阶段时，＼+·a+＼+·t都有Token，而＼+·a+＼+·t=＼+·a+＼+·t-P，这等于t被触发的＼+·t＼+＼{post＼}，因此约简后通信变迁t能够被触发。根据约简前满足协同正确性及定义1可知，通信变迁t能够执行完成。

（2）如果P≠，则可以推出合并后通信变迁t能够被触发，必须满足＼+·a+＼+·t-P都有Token，而＼+·t=＼+·e+a＼+·∩t＼+·，即t的前集由两部分组成，一部分为外部提供的Token，另一部分为a提供的Token。由＼+·t =＼+·e+P可知，＼+·e=＼+·t-P，则可以推出合并后运行到该阶段时，＼+·e+＼+·a都有Token，而这等于t被触发的＼+·t＼+＼{post＼}，因此约简后通信变迁t能够被触发。根据约简前满足协同正确性及定义1可知，通信变迁t能够执行完成。

不管在哪种情况下，通信变迁t都能够执行完成，在执行完成后内部其它与a和t存在约束关系的变迁也都能够被触发。根据约简前满足协同正确性及定义1可知，与之存在消息依赖关系的组织都可以执行完成，从而推导出约简后的组织和协同组织都可以正确地执行完毕，满足协同正确性。

τ；τ≈τ和τ.τ≈τ可以看作规则1的特例。

约简规则2：令α为某个通信变迁生成的通信行为视图，τ为某个瞬时变迁对应的行为，则α；τ可以约简为α，记为α；τ≈α。

证明过程与规则1类似，略。

约简规则3：令α、β为两个通信变迁生成的通信行为视图，τ为某个瞬时变迁对应的行为，则α+τ；β可以约简为α+β，记为α+τ；β≈α+β。其中，+表示兩个进程的选择执行。

证明： （1）如果左边的α进程对应的变迁t能够被触发，根据约简前满足协同正确性，可以推出约简后也满足协同正确性。

（2）如果选择右边的分支执行，因为τ和进程β是顺序执行的，根据规则1可知，约简后也满足协同正确性。

约简规则4 ：令α、β为两个通信变迁生成的通信行为视图，τ为某个瞬时变迁对应的行为，则α+β；τ可以约简为α+β，记为α+β；τ≈α+β。其中，+表示两个进程的选择执行。

证明过程与规则3类似，略。

规则3和规则4考虑了异步通信对协同正确性的影响，它没有声称α+τ≈α，是因为其可能因异步通信而导致协同的不正确性，见命题1。

命题1：用α替换α+τ可能导致业务过程不满足协同正确性。

证明：设协同环境为R，α+τ所在的组织为org。当org执行到状态M时，可以选择一个活动执行，分两种情况讨论：①当选择内部活动执行时，因为org和环境R能够正确协同，在R中必存在一个不依赖于该选择阶段的内部活动，即R′→τP，其中，R′为R执行到该阶段时所处的状态；②当选择通信活动执行时，推出R中必存在相关的消息依赖活动。假如通信活动的执行由外部活动rs发送消息而触发，即R′→rsQ。因为内部活动和通信活动的执行是互斥的，则推出R′→τP和R′→rsQ发生也是互斥的，即R′=τ.P+rs.Q，进而替换后的org与R在该阶段一次可能的交互为：α|（τ.P+rs.Q）→τα|P。由定义1可知，由于α得不到rs发送的消息而阻塞，导致org发生死锁，进而引起业务过程协同的失败，即不满足协同正确性。

约简规则5：令α、β为两个通信变迁生成的通信行为视图，P为复合进程，τ为某个瞬时变迁对应的行为，则P=（α；β；τ）；P可以约简为（α；β）；P，记为P≈（α；β）；P。

证明：从进程P的执行顺序看，在一次执行过程中，β进程所映射的通信变迁t和τ映射的瞬时变迁a是顺序执行的关系，同时根据合理性定义，进程P的循环次数必须是确定的。因而根据规则1，约简后满足协同正确性。

约简规则6：令α、β为两个通信变迁生成的通信行为视图，P为复合进程，τ为某个瞬时变迁对应的行为，则P=（α；τ；β）；P可以约简为（α；β）；P，记为P≈（α；β）；P。

证明过程与规则5类似，略。

相对于进程代数中的等价理论，约简规则1～6能够放宽验证条件。如α+τ.β和α+β并不弱等价，但是基于规则3，约简后满足协同正确性。

定义4（模型推导） 给定一个业务过程模型，为了找到一个与之等价并具有较小状态空间的业务过程模型，需要首先构造一个可能的业务过程模型，然后根据各自的业务过程模型视图分别构建可达图，找到互模拟关系，并进行行为比较，这种方法称为模型推导。

从定义4可以看出，模型推导需要首先尝试找到一个可能的、具有较小状态空间的业务过程模型，然后分别构建各自的可达图，从可达图上找出互模拟关系进行判定。该方式工作量大并具有相当大的随意性，不利于数学推导，也不利于计算机辅助工具的设计与开发。同时，由于基于互模拟关系验证等价的条件过于苛刻，不能有效地支持状态空间的约简。

定义5（代数推导） 对于一个给定的业务过程模型，利用规则1～6、命题1及CCS中的等价理论可以直接推导生成与该业务过程模型等价并具有较小状态空间的业务过程模型，这种方法称为代数推导。

从定义5可以看出，与模型推导相比，代数推导不需要首先构造出一个可能与之行为等价的，并具有较少状态空间的业务过程模型，只需要利用规则1～6、命题1及CCS中的等价关系进行推导判定，提高了验证效率。同时代数在推导过程中是基于规则1～6的，相对于进程代数中的互模拟关系，弱化了验证条件，能够支持具有更小状态空间的业务过程模型生成。

3 结语

本文针对跨组织业务过程协同进行研究，为了充分反映出跨组织业务过程协同中表现出来的自治、异步及安全保护等特性，引入进程标号迁移系统PLTS对单个参与组织的模型视图和通信行为视图序列进行集成。为了减少验证代价，提出6條约简规则，并证明了满足这6条规则的替换是协同正确的，从而将业务过程行为验证由模型推导转变成代数推导。未来工作将主要针对以下2个方面问题进行研究：①原型系统实现；②如何对生成的行为进程进行一致性验证。

参考文献：

[1] 卢亚辉，明仲，张力.业务过程协同模式的研究[J].计算机集成制造系统，2011，17（8）：1570-1579.

[2] M L ROSA， A TER HOFSTEDE， P WOHED， et al.Managing process model complexity via concrete syntax modifications[J]. IEEE Transactions on Industrial Informatics， 2011，7（2）：255-265.

[3] M L ROSA， P WOHED， J MENDLING， et al.Managing process model complexity via abstract syntax modifications[J]. IEEE Trans. Ind. Informat， 2011，7（4）：614-629.

[4] S LI， L XU， X WANG， et al.Integration of hybrid wireless networks in cloud services oriented enterprise information systems[J].Enterprise Inform，Syst，2012，6（2）：165-187.

[5] K WANG， X BAI， J LI，et al.A service-based framework for pharmacogenomics data integration[J]. Enterprise Inform. Syst， 2010，4（3）：225-245.

[6] L XU.Enterprise systems： state-of-the-art and future trends[J].IEEE Trans. Ind. Informat， 2011，7（4）：630-640.

[7] M ZDRAVKOVI， H PANETTO， M TRAJANOVIC，et al.An approach for formalizing the supply chain operations[J].Enterprise Inform. Syst， 2011，5（4）：401-421.

[8] J GUO， L XU， Z GONG，et al.Semantic inference on heterogeneous e-marketplace activities[J].IEEE Trans. Syst.， Man， Cybern.—Part A： Syst. Humans， 2012，42（2）：316-330.

[9] J GUO.Collaboration role in semantic integration for electronic marketplace[J].Int. J. Electron. Bus， 2010，8（6）：528-549.

[10] VAN DER AALST WMP. Modeling and analyzing interorganizational workflows[C].Proceedings of the 1st International Conference on Application of Concurrency to System Design（CSD'98）， Fukushima. Washington， DC， USA： IEEE Computer Society， 1998：262-272.

（責任编辑：黄 健）