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

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