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

计算机科学 ›› 2018, Vol. 45 ›› Issue (11A): 597-602.

• 综合、交叉与应用 • 上一篇

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

赵莹¹, 潘华², 张云猛², 莫启³, 代飞⁴

云南电力调度控制中心昆明650011¹
云南云电同方科技有限公司昆明650217²
云南大学软件学院昆明650091³
西南林业大学大数据与智能工程学院昆明650224⁴

出版日期:2019-02-26 发布日期:2019-02-26
通讯作者: 代飞(1982-),男,博士,副教授,主要研究方向为业务过程和软件工程,E-mail:59671019@qq.com
作者简介:赵莹(1983-),女,高级工程师,主要研究方向为电力调度自动化与信息化;潘华(1983-),男,高级工程师,主要研究方向为电力调度信息系统;张云猛(1987-),男,主要研究方向为电力调度信息系统研究与管理;莫启(1986-),男,博士,讲师,主要研究方向为业务过程和软件工程
基金资助:
本文受国家自然科学基金(61462095,61702442),云南省自然科学基金(2016FB102)资助。

Modeling and Behavior Verification for Collaborative Business Processes

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⁴

Online:2019-02-26 Published:2019-02-26

摘要/Abstract

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

关键词: 模型检测, 协同业务过程, 行为验证, 业务过程, 异步消息通信

Abstract: 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.

Key words: Asynchronous message communication, Behavior verification, Business process, Collaborative business process, Model checking

中图分类号:

TP311

赵莹, 潘华, 张云猛, 莫启, 代飞. 协同业务过程建模与行为验证[J]. 计算机科学, 2018, 45(11A): 597-602. https://doi.org/

ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes[J]. Computer Science, 2018, 45(11A): 597-602. https://doi.org/

参考文献

[1]代飞,莫启,林雷蕾,等.结合Petri网和Pi演算的协同业务过程建模[J].计算机科学与探索,2015,9(6):692-706.
[2]卢亚辉,明仲,张力.业务过程协同模式的研究[J].计算机集成制造系统,2011,17(8):1570-1579.
[3]YU W Y,YAN C G,DING Z J,et al.Modeling and verification of online shopping business processes by considering malicious behavior patterns[J].IEEE Transactions on Automation Science and Engineering,2016,13(2):647-662.
[4]SHAHRIARI K,HESSAMI A G,JADIDI A,et al.An approach toward a conceptual collaborative framework based on a case study in a wood supply chain[J].IEEE Systems Journal,2015,9(4):1-10.
[5]曾庆田,鲁法明,刘聪,等.基于Petri网的跨组织应急联动处置系统建模与分析[J].计算机学报,2013,36(11):2290-2302.
[6]KESTEN Y,PNUELI A,RAVIV L O.Algorithmic verification of linear temporal logic specifications[J].Lecture Notes in Computer Science,1999,1443(1443):1-16.
[7]CS Department NUS.PAT:Process Analysis Toolkit [EB/OL].[2013-09-13].http://www.patroot.com.
[8]AALST W.Modeling and analyzing interorganizational work-flows[C]∥Proc of the 1st IntConf on Application of Concurrency to System Design.Los Alamitos,CA:IEEE Computer Society,1998:262-272.
[9]ZHANG L,LU Y,XU F.Unified modelling and analysis of collaboration business process based on Petri nets and Pi calculus[J].IET Software,2010,4(5):303-317.
[10]ZENG Q T,LU F M,LIU C,et al.Modeling and verification for cross-department collaborative business processes using exte-nded Petri nets[J].IEEE Trans on Systems,Man,and Cyberne-tics:Systems,2015,45(2):349-362.
[11]葛季栋,胡海洋,周宇,等.一种基于不变量的工作流协同模型分解方法[J].计算机学报,2012,35(10):2169-2181.
[12]邓水光,李莹,吴健,等.Web服务行为兼容性的判定与计算[J].软件学报,2007,18(12):3001-3014.
[13]AALST W,PESIC M,SCHONENBERG H.Declarative workflows:Balancing between flexibility and support[J].Computer Science-Research and Development,2009,23(2):99-113.
[14]MONTALI M.Specification and verification of declarative open interaction models-A logic-based approach[J].Springer Science &Business Media,2010,56(1):47-76.
[15]HIDEBRANDT T,MUKKAMALA R.Declarative event-based workflow as distributed dynamic condition response graphs[C]∥Electronic Proceedings in Theoretical Computer Science(EPTCS) 69:Proc of PLACES 2010.Sydney,Australia:EPTCS,2011:59-73.
[16]AWAD A,WEIDLICH M,WESKE M.Visually specifying compliance rules and explaining their violations for business process[J].Journal of Visual Languages & Computing,2011,22 (1):30-55.
[17]BAIER C,KATOEN J P.Principles of model checking[M].ambridge:MIT Press,2008.
[18]SUN J,LIU Y,DONG J S.Model Checking CSP Revisited:Introduc-ing a Process Analysis Toolkit[M]∥Leveraging Applications of Formal Methods,Verification and Validation.Springer Berlin Heidelberg,2008:307-322.

相关文章 15

[1]	冉丹, 陈哲, 孙毅, 杨志斌. 基于程序转化的SCADE模型检测 SCADE Model Checking Based on Program Transformation 计算机科学, 2021, 48(12): 125-130. https://doi.org/10.11896/jsjkx.201100080
[2]	蔡泳, 钱俊彦, 潘海玉. 基于度量线性时态逻辑的近似安全性 Approximate Safety Properties in Metric Linear Temporal Logic 计算机科学, 2020, 47(10): 309-314. https://doi.org/10.11896/jsjkx.191000175
[3]	夏奴奴, 杨晋吉, 赵淦森, 莫晓珊. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证 Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model 计算机科学, 2019, 46(8): 206-211. https://doi.org/10.11896/j.issn.1002-137X.2019.08.034
[4]	韩英杰, 周清雷, 朱维军. 基于DNA计算的计算树逻辑模型检测方法研究进展 Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking 计算机科学, 2019, 46(11): 25-31. https://doi.org/10.11896/jsjkx.181102091
[5]	周女琪, 周宇. 基于概率模型检测的Web服务组合多目标验证 Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking 计算机科学, 2018, 45(8): 288-294. https://doi.org/10.11896/j.issn.1002-137X.2018.08.052
[6]	曹蕊, 方贤文, 王丽丽. 基于通讯行为轮廓挖掘条件非频繁行为的方法 Method of Mining Conditional Infrequent Behavior Based on Communication Behavior Profile 计算机科学, 2018, 45(8): 310-314. https://doi.org/10.11896/j.issn.1002-137X.2018.08.056
[7]	雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究 Parallelization of LTL Model Checking Based on Possibility Measure 计算机科学, 2018, 45(4): 71-75. https://doi.org/10.11896/j.issn.1002-137X.2018.04.010
[8]	聂凯,周清雷,朱维军,张朝阳. 基于时序逻辑的3种网络攻击建模 Modeling for Three Kinds of Network Attacks Based on Temporal Logic 计算机科学, 2018, 45(2): 209-214. https://doi.org/10.11896/j.issn.1002-137X.2018.02.036
[9]	杨红, 洪玫, 屈媛媛. 基于模型检测技术的变异测试用例生成方法 Approach of Mutation Test Case Generation Based on Model Checking 计算机科学, 2018, 45(11A): 488-493.
[10]	赵莹, 赵川, 黄苾, 代飞. BPMN 2.0过程模型的语义和分析 Semantics and Analysis of BPMN 2.0 Process Models 计算机科学, 2018, 45(11A): 558-563.
[11]	刘爽, 魏欧, 郭宗豪. 基于概率模型检测和遗传算法的基因调控网络的无限范围优化控制 Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm 计算机科学, 2018, 45(10): 313-319. https://doi.org/10.11896／j.issn.1002-137X.2018.10.058
[12]	杜伊,何洋,洪玫. 概率模型检测在动态能耗管理中的应用 Application of Probabilistic Model Checking in Dynamic Power Management 计算机科学, 2018, 45(1): 261-266. https://doi.org/10.11896/j.issn.1002-137X.2018.01.046
[13]	高婉玲,洪玫,杨秋辉,赵鹤. 统计算法选择对统计模型检测效率的影响分析 Efficiency Analysis of Different Statistical Algorithms on Statistical Model Checking 计算机科学, 2017, 44(Z6): 499-503. https://doi.org/10.11896/j.issn.1002-137X.2017.6A.111
[14]	曾赛文,文中华,戴良伟,袁润. 基于不确定攻击图的攻击路径的网络安全分析 Analysis of Network Security Based on Uncertain Attack Graph Path 计算机科学, 2017, 44(Z6): 351-355. https://doi.org/10.11896/j.issn.1002-137X.2017.6A.080
[15]	屈媛媛,洪玫,孙琳. 多核系统动态温度管理TAPE策略的形式化验证 Formal Verification of TAPE Strategy for Dynamic Temperature Management in Multi-core System 计算机科学, 2017, 44(Z11): 542-546. https://doi.org/10.11896/j.issn.1002-137X.2017.11A.115

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed