协同业务过程建模与行为验证

Modeling and Behavior Verification for Collaborative Business Processes

对协同业务过程进行建模和行为验证是确保业务过程正确实施的关键。文中提出了一种协同业务过程的建模和行为验证方法。首先,该方法使用有限状态自动机建模每个参与组织的业务过程,并通过集中式消息缓冲区,将业务过程异步组合为协同业务过程;其次,提出了行为约束的声明式模板,用于定义协同业务过程中的行为约束关系,并通过映射规则,将行为约束关系转换为LTL(Linear Temporal Logic)公式;最后,提出了行为验证框架,借助进程分析工具PAT,实现了对协同业务过程行为的自动验证。通过对电力突发公共事件应急处置系统的建模与行为验证,阐述了所提方法的可行性和有效性。

Modeling and behavior verification for collaborative business processes is the key to ensure enactment right of business process.This paper proposed an approach to model and verify behavior of collaborative business processes.Firstly,this method uses finite state automaton to model each peer’s business process and composes them into the collaborative business process under the asynchronous communication model through the centralized message buffer.Se-condly,the declarative template is given for behavior constraint,which is used to define the behavior constraint relationship in collaborative business processes.This behavior constraint specification can be converted to LTL formula by mapping rules.Finally,the framework of behavior verification is proposed to automatically check the behavior of collaborative business processes with the help of PAT(Process Analysis Toolkit).The feasibility and effectiveness of this me-thod were proved through the modeling and behavior verification of emergency response system for public emergency public events.