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: Collaborative business process, Business process, Asynchronous message communication, Behavior verification, Model checking

CLC Number: 

  • TP311
[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.
[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].
[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.
[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] LUO Xiang-yu, XU Hang-na, ZENG Hao-cheng, CHEN Zu-xi, YANG Fan. Symbolic Model Checking for Discrete Real-time Linear Dynamic Logic [J]. Computer Science, 2020, 47(9): 204-212.
[2] CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314.
[3] 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.
[4] 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.
[5] 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.
[6] 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.
[7] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[8] 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.
[9] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[10] 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.
[11] 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.
[12] 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.
[13] 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.
[14] DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266.
[15] GAO Ya-nan, FANG Xian-wen and WANG Li-li. Optimized Analysis of Business Process Configuration Based on Petri Net Behavior Closeness [J]. Computer Science, 2017, 44(Z6): 539-542.
Full text



[1] . [J]. Computer Science, 2018, 1(1): 1 .
[2] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75 .
[3] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[4] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[5] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[6] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99 .
[7] ZHOU Yan-ping and YE Qiao-lin. L1-norm Distance Based Least Squares Twin Support Vector Machine[J]. Computer Science, 2018, 45(4): 100 -105 .
[8] LIU Bo-yi, TANG Xiang-yan and CHENG Jie-ren. Recognition Method for Corn Borer Based on Templates Matching in Muliple Growth Periods[J]. Computer Science, 2018, 45(4): 106 -111 .
[9] GENG Hai-jun, SHI Xin-gang, WANG Zhi-liang, YIN Xia and YIN Shao-ping. Energy-efficient Intra-domain Routing Algorithm Based on Directed Acyclic Graph[J]. Computer Science, 2018, 45(4): 112 -116 .
[10] CUI Qiong, LI Jian-hua, WANG Hong and NAN Ming-li. Resilience Analysis Model of Networked Command Information System Based on Node Repairability[J]. Computer Science, 2018, 45(4): 117 -121 .