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

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.