Verifiable Model Construction for Business Processes
Abstract
Business process specified in Business Process Execution Language (BPEL), which integrates existing services to develop composite service for offering more complicated function, is error-prone. Verification and testing are necessary to ensure the correctness of business processes. SPIN, for which the input language is PROcess MEta-LAnguage (Promela), is one of the most popular tools for detecting software defects and can be used both in verification and testing. In this paper, an automatic approach is proposed to construct the verifiable model for BPEL-based business process with Promela language. Business process is translated to an intermediate two-level representation, in which eXtended Control Flow Graph (XCFG) describes the behavior of BPEL process in the first level and Web Service Description Models (WSDM) depict the interface information of composite service and partner services in the second level. With XCFG of BPEL process, XCFGs for partner services are generated to describe their behavior. Promela model is constructed by defining data types based on WSDM and defining channels, variables and processes based on XCFGs. The constructed Promela model is closed, containing not only the BPEL process but also its execution environment. Case study shows that the proposed approach is effective.
References
- 1. , Optimal control based regression test selection for service-oriented workflow applications, J. Syst. Softw. 124 (2017) 274–288. Crossref, Web of Science, Google Scholar
- 2. A. Alves, A. Arkin and S. Askary, Web services business process execution language version 2.0, OASIS Standard, 2007, http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html. Google Scholar
- 3. , Model-checking behavioral specification of BPEL applications, Electron. Notes Theor. Comput. Sci. 151 (2006) 89–105. Crossref, Google Scholar
- 4. , Spin Model Checker: The Primer and Reference Manual (Addison-Wesley, Boston, 2003). Google Scholar
- 5. , A rule-based language and verification framework of dynamic service composition, Future Internet 12(2) (2020) 23. Crossref, Web of Science, Google Scholar
- 6. , Generation test cases specifications for BPEL compositions of web services using SPIN, in Proc. Int. Workshop on Web Services Modeling and Testing, 2006, pp. 83–94. Google Scholar
- 7. , Analysis of interacting BPEL web services, in Proc. 13th Int. Conf. World Wide Web, 2004, pp. 621–630. Crossref, Google Scholar
- 8. , A method of verifying web service composition, in Proc. 2010 Symp. Information and Communication Technology, 2010, pp. 155–162. Crossref, Google Scholar
- 9. E. Christensen, F. Curbera, G. Meredith and S. Weerawarana, Web services description language (WSDL) 1.1. W3C note, 2001, http://www.w3.org/TR/2001/NOTE-wsdl-20010315. Google Scholar
- 10. , Test case selection for all-uses criterion-based regression testing of composite service, IEEE Access 7 (2019) 174438–174464. Crossref, Web of Science, Google Scholar
- 11. , Conflict detection in composite web services based on model checking, Int. J. Web Grid Serv. 9(4) (2013) 394–430. Crossref, Web of Science, Google Scholar
- 12. , Automatic test case selection for regression testing of composite service based on extensible BPEL flow graph, J. Syst. Softw. 85 (2012) 1300–1324. Crossref, Web of Science, Google Scholar
- 13. , Verifying cloud application for the interaction correctness using SoaML and SPIN, in Proc. 2019 8th Int. Conf. Software and Computer Applications, 2019, pp. 210–216. Crossref, Google Scholar
- 14. , Formalizing time Petri nets with metric temporal logic using Promela, in Proc. 20th IEEE/ACIS Int. Conf. Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, 2019, pp. 162–166. Crossref, Google Scholar
- 15. , Correctness of an ATL model transformation from SysML state machine diagrams to Promela, in Proc. 8th Int. Conf. Model-Driven Engineering and Software Development, 2020, pp. 360–372. Crossref, Google Scholar
- 16. , Behavioral interface conformance checking for WS-BPEL processes, in Proc. 2008 Int. MCETECH Conf. e-Technologies, 2008, pp. 253–257. Crossref, Google Scholar
- 17. R. Nakashiro, Y. Kamei, N. Ubayashi, S. Nakajima and A. Iwai, Translation pattern of BPEL process into Promela code, in Proc. 2011 Joint Conf. 21st Int. Workshop on Software Measurement and the 6th Int. Conf. Software Process and Product Measurement, 2011, pp. 285–290. Google Scholar
- 18. , Formal verification of cloud orchestration design with TOSCA and BPEL, in Proc. 2016 13th Int. Conf. Electrical Engineering/Electronics, Computer, Telecommunications and Information Technology, 2016, pp. 1–5. Crossref, Google Scholar
- 19. , BPELVT: A tool for formal validation of web service orchestrations, in Proc. 2012 IEEE 21st Int. WETICE, 2012, pp. 426–428. Crossref, Google Scholar
- 20. , Safety verification of RGPS service layer meta-model, Adv. Comput. Sci. Res. 77 (2018) 10–14. Google Scholar
- 21. , A model checking based test case generation framework for web services, in Proc. Int. Conf. Information Technology, 2007, pp. 715–722. Google Scholar
- 22. , An automatic test case generation framework for web services, J. Softw. 2(3) (2007) 64–77. Crossref, Google Scholar
- 23. , Model checking WS-BPEL with universal modal sequence diagrams, in Proc. 2011 10th IEEE/ACIS Int. Conf. Computer and Information Science, 2011, pp. 328–333. Crossref, Google Scholar
- 24. , Verification of behavior-aware privacy requirements in web services composition, J. Softw. 9(4) (2014) 944–951. Crossref, Google Scholar
- 25. , Towards model-based verification of BPEL with model checking, in Proc. Sixth IEEE Int. Conf. Computer and Information Technology, 2006, p. 190. Crossref, Google Scholar
- 26. , View: An incremental approach to verify evolving workflows, in Proc. 34th ACM/SIGAPP Symp. Applied Computing, 2019, pp. 85–93. Crossref, Google Scholar
| Remember to check out the Most Cited Articles! |
|---|
|
Check out our titles in C++ Programming! |
