计算机科学 ›› 2018, Vol. 45 ›› Issue (11A): 597-602.
• 综合、交叉与应用 • 上一篇
赵莹1, 潘华2, 张云猛2, 莫启3, 代飞4
ZHAO Ying1, PAN Hua2, ZHANG Yun-meng2, MO Qi3, DAI Fei4
摘要： 对协同业务过程进行建模和行为验证是确保业务过程正确实施的关键。文中提出了一种协同业务过程的建模和行为验证方法。首先,该方法使用有限状态自动机建模每个参与组织的业务过程,并通过集中式消息缓冲区,将业务过程异步组合为协同业务过程;其次,提出了行为约束的声明式模板,用于定义协同业务过程中的行为约束关系,并通过映射规则,将行为约束关系转换为LTL(Linear Temporal Logic)公式;最后,提出了行为验证框架,借助进程分析工具PAT,实现了对协同业务过程行为的自动验证。通过对电力突发公共事件应急处置系统的建模与行为验证,阐述了所提方法的可行性和有效性。
中图分类号:
| [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. |
| [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 |
|
||
首页