Computer Science ›› 2018, Vol. 45 ›› Issue (11A): 597-602.

• Interdiscipline & Application • Previous Articles    

Modeling and Behavior Verification for Collaborative Business Processes

ZHAO Ying1, PAN Hua2, ZHANG Yun-meng2, MO Qi3, DAI Fei4   

  1. Yunnan Power Dispatching and Control Center,Kunming 650011,China1
    Yunnan Yundian Tongfang Technology Co.,Ltd.,Kunming 650217,China2
    School of Software,Yunnan University,Kunming 650091,China3
    School of Big Data and Intelligence Engineering,Southwest Forestry University,Kunming 650224,China4
  • Online:2019-02-26 Published:2019-02-26

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

CLC Number: 

  • TP311
[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] ZHANG Ji-lin, SHAO Yu-cao, REN Yong-jian, YUAN Jun-feng, WAN Jian, ZHOU Li. Dynamic Customization Model of Business Processes Supporting Multi-tenant [J]. Computer Science, 2022, 49(6A): 705-713.
[2] RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130.
[3] CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314.
[4] XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211.
[5] HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun. Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking [J]. Computer Science, 2019, 46(11): 25-31.
[6] ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294.
[7] CAO Rui, FANG Xian-wen, WANG Li-li. Method of Mining Conditional Infrequent Behavior Based on Communication Behavior Profile [J]. Computer Science, 2018, 45(8): 310-314.
[8] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[9] HE Lu-lu, FANG Huan. Change Propagation Method of Service-oriented Business Process Model with Data Flows Based on Petri Net [J]. Computer Science, 2018, 45(6A): 545-548.
[10] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[11] NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214.
[12] YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493.
[13] ZHAO Ying, ZHAO Chuan, HUANG Bi, DAI Fei. Semantics and Analysis of BPMN 2.0 Process Models [J]. Computer Science, 2018, 45(11A): 558-563.
[14] LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319.
[15] DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!