{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:54:59Z","timestamp":1781106899224,"version":"3.54.1"},"reference-count":20,"publisher":"IGI Global Scientific Publishing","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,1,1]]},"abstract":"<p>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.<\/p>","DOI":"10.4018\/ijeis.2020010105","type":"journal-article","created":{"date-parts":[[2019,11,29]],"date-time":"2019-11-29T04:50:03Z","timestamp":1575003003000},"page":"92-107","source":"Crossref","is-referenced-by-count":3,"title":["A New Business Process Verification Approach for E-Commerce Using Petri Nets"],"prefix":"10.4018","volume":"16","author":[{"given":"Mei","family":"Zhang","sequence":"first","affiliation":[{"name":"Guizhou University of Finance and Economics, Guizhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fei","family":"Feng","sequence":"additional","affiliation":[{"name":"Guizhou University of Finance and Economics, Guizhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhilong","family":"Zhang","sequence":"additional","affiliation":[{"name":"Guizhou University of Finance and Economics, Guizhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jinghua","family":"Wen","sequence":"additional","affiliation":[{"name":"Guizhou University of Finance and Economics, Guizhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"issue":"1","key":"IJEIS.2020010105-0","first-page":"87","article-title":"An extension to BPEL for criteria-based web service composition.","volume":"13","year":"2016","journal-title":"International Journal on Computer Science and Engineering"},{"key":"IJEIS.2020010105-1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-10-1837-4_76"},{"key":"IJEIS.2020010105-2","unstructured":"Chhabra, A., Sangroya, A., & Anantaram, C. (2018). Formalizing and verifying natural language system requirements using petri nets and context based reasoning. Proceedings of the 10th International Workshop Modelling and Reasoning in Context, co-located with the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018 and the 23rd European Conference on Artificial Intelligence, ECAI 2018."},{"key":"IJEIS.2020010105-3","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.04.014"},{"key":"IJEIS.2020010105-4","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.4699"},{"key":"IJEIS.2020010105-5","author":"H.Jahan","year":"2017","journal-title":"Test Case Generation fbr BPEL-Based Web Service Composition Using Colored Petri Net"},{"key":"IJEIS.2020010105-6","author":"H.Jahan","year":"2017","journal-title":"Test Case Generation for BPEL-Based Web Service Composition Using Colored Petri Net"},{"issue":"2","key":"IJEIS.2020010105-7","first-page":"26","article-title":"Based on the temporal specification of TLA and TLC model checking.","volume":"10","author":"Z. H. A. N. G.Jun-ming","year":"2015","journal-title":"Journal of Guiyang College Natural Sciences (Quarterly)"},{"key":"IJEIS.2020010105-8","doi-asserted-by":"publisher","DOI":"10.15388\/Informatica.2015.71"},{"key":"IJEIS.2020010105-9","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/j.ins.2017.03.014","article-title":"Petri net representation and reachability analysis of 0\u20131 integer linear programming problems.","volume":"400-401","year":"2017","journal-title":"Information Sciences"},{"key":"IJEIS.2020010105-10","unstructured":"Li, Tang, & Zhang. (2016). Multilateral Cooperation Intrusion Forensics Based on Temporal Logic of Action. Cyberspace Security, (11-12), 82-86."},{"key":"IJEIS.2020010105-11","author":"Z.Liu","year":"2015","journal-title":"Description and verification of network protocol based on behavior temporal logic TLA"},{"issue":"1-2","key":"IJEIS.2020010105-12","first-page":"82","article-title":"Transformation from business process models to BPEL with overlapped patterns involved.","volume":"9","author":"Z.Man","year":"2016","journal-title":"International Journal of High Performance Computing and Networking"},{"key":"IJEIS.2020010105-13","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2016.01.001"},{"issue":"4","key":"IJEIS.2020010105-14","first-page":"895","article-title":"Optimized Mutation Testing Techniques for WS-BPEL Programs.","volume":"56","author":"C.Sun","year":"2019","journal-title":"Journal of Computer Research and Development"},{"key":"IJEIS.2020010105-15","author":"Y.Wang","year":"2019","journal-title":"Study on Optimization of Credit Business Process of Y Rural Commercial Bank Based on BPR"},{"key":"IJEIS.2020010105-16","unstructured":"Xiong, F. (2018). Business Process Design of E-commerce Platform Based on B2C mode. Logistics Engineering and Management, 40(8), 93-94."},{"key":"IJEIS.2020010105-17","author":"A.Yin","year":"2018","journal-title":"On Optimized Deadlock Control for Petri Nets Based on Structural and Reachability Graph Analysis"},{"issue":"6","key":"IJEIS.2020010105-18","first-page":"22","article-title":"Modeling and analyzing BPEL processes under dead path elimination semantics.","volume":"36","author":"C.Ying","year":"2017","journal-title":"Microcomputer & Its Applications"},{"key":"IJEIS.2020010105-19","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2018.04.090"}],"container-title":["International Journal of Enterprise Information Systems"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=243705","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T11:56:46Z","timestamp":1651838206000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/IJEIS.2020010105"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2020,1,1]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1]]}},"URL":"https:\/\/doi.org\/10.4018\/ijeis.2020010105","relation":{},"ISSN":["1548-1115","1548-1123"],"issn-type":[{"value":"1548-1115","type":"print"},{"value":"1548-1123","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,1,1]]}}}