Formal design and verification of business processes

被引：0

作者：

Ding M. ^{[1
,2
]}

Zhang S.-L. ^{[1
]}

Zhang C. ^{[3
]}

机构：

[1] School of Information and Technology, Northwest University, Xi'an, 710127, Shaanxi

[2] Xi'an Aeronautics Computing Technique Research Institute, AVIC, Xi'an, 710119, Shaanxi

[3] School of Computer Science and Technology, Xidian University, Xi'an, 710071, Shaanxi

来源：

Beijing Ligong Daxue Xuebao/Transaction of Beijing Institute of Technology | 2016年 / 36卷 / 11期

关键词：

Business process; Deterministic finite automata; Linear temporal logic; Model checking;

D O I：

10.15918/j.tbit1001-0645.2016.11.010

中图分类号：

学科分类号：

摘要：

To ensure the consistency of business process design models and business requirements, based on the researches on finite automata model, a quantitative method was proposed in this paper to deal with the construction and verification of business process models. First, the extended conditioned deterministic finite automata were used to describe business process design models and linear temporal logic was used to represent business requirements. Furthermore, the algorithms for transforming the business process design models into automata models and the automata model into Promela were presented. Finally, based on the model checking method, the consistency of the design models and properties were verified with the Spin, if the system models could not satisfy the property, a counter-example and the execution path could be found. Experimental results show that the proposed method is useful in ensuring the correctness of business process design. © 2016, Editorial Department of Transaction of Beijing Institute of Technology. All right reserved.

引用

页码：1147 / 1153

页数：6

共 16 条

[1]

Ingo W., Jorg H., Jan M., Semantic business process validation, Proceedings of the 3rd International Workshop on Semantic Business Process Management, pp. 22-36, (2009)

[2]

Qiu X., Zheng J., Tang Y., Et al., Executive validation analysis of workflow process, Proceedings of the 5th World Congress on Intelligent Control and Automation, pp. 2702-2705, (2004)

[3]

Masalagiu C., Chin W.N., Andrei S., Et al., A rigorous methodology for specification and Turin verification of business processes, Formal Aspects of Computing, 21, 5, pp. 495-510, (2009)

[4]

Van Hee K.M., Sidorova N., Van Der Werf J.M., Business process modeling using Petri nets, Transactions on Petri Nets and Other Models of Concurrency VII, LNCS 7480, pp. 116-161, (2013)

[5]

Lei L., Duan Z., An extended deterministic finite automata based method for the verification of composite web services, Journal of Software, 18, 12, pp. 2980-2990, (2007)

[6]

Liu Y., Muller S., Xu K., A static compliance checking framework for business process models, IBM Systems Journal, 46, 2, pp. 335-361, (2006)

[7]

Yuan M., Huang Z., Li X., Et al., Towards a formal verification approach for business process coordination, Proceedings of 2010 IEEE Eighth International Conference on Web Services, pp. 362-368, (2010)

[8]

Song B., Wang J., Yu G., Verification method for process model based on graph-spreading and graph-reduction, Mini-Micro Systems, 26, 6, pp. 1073-1078, (2005)

[9]

Sadiq W., Orlowska M.E., Analyzing process models using graph reduction techniques, Information Systems, 25, 2, pp. 117-134, (2000)

[10]

Groefsema H., Bucur D., A survey of formal business process verification: from soundness to variability, Proceedings of International Symposium on Business Modeling and Software Design (BMSD), pp. 198-203, (2013)

← 1 2 →