Annals of Computer Science and Information Systems, Volume 17

DOI: http://dx.doi.org/10.15439/2018F148

Citation: Communication Papers of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 17, pages 241–247 (2018)

Full text

Abstract. This paper studies verification of programs similar to BPEL4WS (BPEL), the latter being a de facto standard for the web services composition and orchestration. Traditionally, in verification of concurrent and distributed programs, the model was either based on shared variables or message passing and was studied separately. BPEL-like programs have features that are present in both models: several flows within one service can be executed in parallel and they can access shared variables, whereas several services communicate by message passing. Therefore, it is natural that for verification of BPEL-like programs, the verification methods developed for shared variables and message passing be integrated. In this paper, we combine the proof rules for shared variable programs from Owicki and Gries, the proof rules for CSP like programs from Apt, Francez and de Roever, together with proof rules for compensation and fault handling, to cover all major features of BPEL. An operational semantics is presented and the proof rules can be justified over that. Examples are provided to show the feasibility of verification framework.

References

1. S. Thatte, XLANG: Web Service for Business Process Design. Microsoft, 2001, http://www.gotdotnet.com/team/xml wsspecs/xlang-c/default.html.
2. F. Leymann, Web Services Flow Language (WSFL 1.0). IBM, 2001, http://www-3.ibm.com/software/solutions/webservices/pdf/WSDL.pdf.
3. F. Curbera, Y. Goland, J. Klein, F. Leymann, D. Roller, M. Satish Thatte, and S. Weerawarana, Business Process Execution Language for Web Service, 2003, http://www.siebel.com/bpel.
4. M. J. Butler and C. Ferreira, “An operational semantics for StAC, a language for modelling long-running business transactions,” in Proc. COORDINATION 2004: 6th International Conference on Coordination Models and Languages, Pisa, Italy, February 24–27, 2004, ser. Lecture Notes in Computer Science, vol. 2949. Springer-Verlag, 2004, pp. 87–104.
5. S. S. Owicki and D. Gries, “An axiomatic proof technique for parallel programs I,” Acta Informatica, vol. 6, pp. 319–340, 1976. http://dx.doi.org/10.1007/BF00268134. [Online]. Available: https://link.springer.com/article/10.1007/BF00268134
6. K. R. Apt, N. Francez, and W. P. D. Roever, “A proof system for communicating sequential processes,” vol. 2, no. 3, pp. 359–385. http://dx.doi.org/10.1145/357103.357110. [Online]. Available: http://dl.acm.org/citation.cfm?id=357110
7. Z. Qiu, S. Wang, G. Pu, and X. Zhao, “Semantics of BPEL4WS-Like fault and compensation handling,” in Proc. FM 2005: International Symposium of Formal Methods Europe, Newcastle, UK, July 18–22, 2005, ser. Lecture Notes in Computer Science, vol. 3582. Springer-Verlag, 2005, pp. 350–365.
8. H. Zhu, Q. Xu, C. Ma, S. Qin, and Z. Qiu, “The rely/guarantee approach to verifying concurrent bpel programs,” in Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, ser. Lecture Notes in Computer Science, vol. 7504. Springer, 2012. http://dx.doi.org/10.1007/978-3-642-33826-7 12 pp. 172–187. [Online]. Available: https://link.springer.com/chapter/10.1007/978-3-642-33826-7_12
9. M. J. Butler and C. Ferreira, “A process compensation language,” in Proc. IFM 2000: 2nd International Conference on Integrated Formal Methods, Dagstuhl Castle, Germany, November 1–3, 2000, ser. Lecture Notes in Computer Science, vol. 1945. Springer-Verlag, 2000, pp. 61–76.
10. M. J. Butler, C. Ferreira, and M. Y. Ng, “Precise modelling of com-pensating business transactions and its application to BPEL,” Journal of Universal Computer Science, vol. 11, no. 5, pp. 712–743, 2005.
11. R. Bruni, H. C. Melgratti, and U. Montanari, “Theoretical foundations for compensations in flow composition languages,” in Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ser. POPL ’05. ACM. http://dx.doi.org/10.1145/1040305.1040323. ISBN 978-1-58113-830-6 pp. 209–220. [Online]. Available: http://doi.acm.org/10.1145/1040305.1040323
12. R. Bruni, G. L. Ferrari, H. C. Melgratti, U. Montanari, D. Strollo, and E. Tuosto, “From theory to practice in transactional composition of web services,” in Formal Techniques for Computer Systems and Business Processes, ser. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. http://dx.doi.org/10.1007/11549970 20 pp. 272–286. [Online]. Available: https://link.springer.com/chapter/10.1007/11549970_20
13. C. Laneve and G. Zavattaro, “Web-pi at work,” in Proc. TGC 2005: International Symposium on Trustworthy Global Computing, Edinburgh, UK, April 7–9, 2005, ser. Lecture Notes in Computer Science, vol. 3705. Springer-Verlag, 2005, pp. 182–194.
14. R. Lanotte, A. Maggiolo-Schettini, P. Milazzo, and A. Troina, “Design and verification of long-running transactions in a timed framework,” Science Computer Programming, vol. 73, no. 2-3, pp. 76–94, 2008. http://dx.doi.org/10.1016/j.scico.2008.07.001. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S0167642308000774
15. C. Luo, S. Qin, and Z. Qiu, “Verifying bpel-like programs with hoare logic,” in Proc. TASE 2008: 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering. Nanjing, China: IEEE Computer Society, June 2008, pp. 151–158.
16. C. B. Jones, “Tentative steps toward a development method for interfering programs,” ACM Trans. Program. Lang. Syst., vol. 5, no. 4, pp. 596–619, 1983. http://dx.doi.org/10.1145/69575.69577. [Online]. Available: http://dl.acm.org/citation.cfm?id=69577
17. W.-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, and M. P. J. Zwiers, Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science 54, Cambridge University Press, 2001.