Article Preview
TopIntroduction
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.