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

Modeling of Cross-Organization Business Process Collaboration Based on Petri Net and Process Algebra

作　　者：笪建 程耀坤 莫启[3] 孙华 吕永华 

机构地区：[1]江苏联合职业技术学院淮安分院信息工程系 [2]淮安开放大学信息工程系,江苏淮安223001 [3]云南大学软件学院,云南昆明650091

出　　处：《软件导刊》2017年第12期49-52,共4页Software Guide

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

关 键 词：PETRI网 进程代数 跨组织业务过程 进程标号迁移系统 约简 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]