摘要
对协同业务过程进行建模和行为验证是确保业务过程正确实施的关键。文中提出了一种协同业务过程的建模和行为验证方法。首先,该方法使用有限状态自动机建模每个参与组织的业务过程,并通过集中式消息缓冲区,将业务过程异步组合为协同业务过程;其次,提出了行为约束的声明式模板,用于定义协同业务过程中的行为约束关系,并通过映射规则,将行为约束关系转换为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.
作者
赵莹
潘华
张云猛
莫启
代飞
ZHAO Ying;PAN Hua;ZHANG Yun-meng;MO Qi;DAI Fei(Yunnan Power Dispatching and Control Center,Kunming 650011,China;Yunnan Yundian Tongfang Technology Co.,Ltd.,Kunming 650217,China;School of Software,Yunnan University,Kunming 650091,China;School of Big Data and Intelligence Engineering, Southwest Forestry University,Kunming 650224,China)
出处
《计算机科学》
CSCD
北大核心
2018年第B11期597-602,共6页
Computer Science
基金
国家自然科学基金(61462095
61702442)
云南省自然科学基金(2016FB102)资助
关键词
协同业务过程
业务过程
异步消息通信
行为验证
模型检测
Collaborative business process
Business process
Asynchronous message communication
Behavior verification
Model checking
