A New Business Process Verification Approach for E-Commerce Using Petri Nets

A New Business Process Verification Approach for E-Commerce Using Petri Nets

Mei Zhang (Guizhou University of Finance and Economics, Guizhou, China), Fei Feng (Guizhou University of Finance and Economics, Guizhou, China), Zhilong Zhang (Guizhou University of Finance and Economics, Guizhou, China) and Jinghua Wen (Guizhou University of Finance and Economics, Guizhou, China)
Copyright: © 2020 |Pages: 16
DOI: 10.4018/IJEIS.2020010105
OnDemand PDF Download:
No Current Special Offers


The design, modeling, optimization, reengineering, and coupling of business processes in e-commerce environment have gradually become a hot research topic. Business processes must be strictly described and validated by formal methods to ensure their reliability and efficiency. This paper systematically studies the introduction of new business process characteristics into behavioral temporal logic and extend TLA to obtain a new logic system PTLA, which enriches the theoretical system of formal method of business process under the environment of e-commerce. The paper also discusses Petri nets and show how to convert Petri nets into TLA. A parallel Petri net model was built to represent the dynamic, concurrency and flexibility, and cross-organizational e-commerce business process. Finally, the use of simulation to extend the business process execution language BPEL to TLA.
Article Preview


E-commerce is quietly changing people's way of life, the success of Amazon, e-Bay, Dangdang and Taobao, showing its broad prospects of development. Business process (Yubo, 2019; Feiyi, 2018) is more efficient and has a great effect on the development of enterprises under the e-commerce environment. Although it has had a series of analysis and modeling methods (Yu et al., 2018) to assist the design of business processes, after the reengineering of business process may still exist a logical flaw and up to less than the enterprise expected target. So it is an inevitable trend to analyze and verify the business process with the aid of formal analysis method. Currently, it is lack of business process which can be more complex and dynamic in the e-commerce environment and a lack of formal method system for the formal analysis and verification.

In the near future, the research on the business process of e-commerce is mainly concerned with the specification and verification of business processes. Such as the use of Petri network, automaton, process algebra specification and verification business service process BPEL (Business Process Execution Language) model (Jahan, 2017; Chhabra, Aishwarya et al., 2018); Chen Ying Firstly put forward a set of rules, realizing the transformation from BPEL under death path elimination semantic to ordinary if-then-else form. Then, this method establishes the formal model of BPEL process using Colored Petri Net (CPN). Finally, the automatic analysis and verification of BPEL process model is accomplished with CPN-Tools.(Chen Ying et al, 2017); Qiang Hu proposed a logic Petri net–based path detecting method for compatibility analysis of interactive service processes, the service process described by WS‐BPEL is modeled as a service net based on logic Petri nets (Qiang Hu et al., 2018). In the literature (Sun Changai et al., 2019), the author mentioned business process execution language for Web service (WS-BPEL) is an executable XML based and process-oriented service composition language. Due to unique features of Web services, such as dynamics, loose coupling, and open deployment and execution environment, it is an important issue how to assure the quality of WS-BPEL programs. The researchers (Zhang Man et al., 2016; Hansen Dominik et al., 2016) also proposed how to transform the UML model into TLA, and using the model checking tool TLC detected the formal description. Hansen Dominik (Hansen Dominik et al., 2016) explores the model checking tool TLC based on TLA+ to speed up the verification of multiple threads and use the disk technology to alleviate the state explosion problem. ZHANG Jun-ming (ZHANG Jun-ming et al., 2015) given the temporal specification model of PCS s by the TLA language and then made use of model checking tool TLC to detect PCS, and finally the property of liveness and mutex were checked.

Complete Article List

Search this Journal:
Volume 18: 4 Issues (2022): Forthcoming, Available for Pre-Order
Volume 17: 4 Issues (2021)
Volume 16: 4 Issues (2020)
Volume 15: 4 Issues (2019)
Volume 14: 4 Issues (2018)
Volume 13: 4 Issues (2017)
Volume 12: 4 Issues (2016)
Volume 11: 4 Issues (2015)
Volume 10: 4 Issues (2014)
Volume 9: 4 Issues (2013)
Volume 8: 4 Issues (2012)
Volume 7: 4 Issues (2011)
Volume 6: 4 Issues (2010)
Volume 5: 4 Issues (2009)
Volume 4: 4 Issues (2008)
Volume 3: 4 Issues (2007)
Volume 2: 4 Issues (2006)
Volume 1: 4 Issues (2005)
View Complete Journal Contents Listing