Verifying BPEL-like programs with Hoare logic

Abstract

The WS-BPEL language has recently become a de facto standard for modeling Web-based business processes. One of its essential features is the fully programmable compensation mechanism. To understand it better, many recent works have mainly focused on formal semantic models for WS-BPEL. In this paper, we make one step forward by investigating the verification problem for business processes written in BPEL-like languages. We propose a set of proof rules in Hoare-logic style as an axiomatic verification system for a BPEL-like core language containing key features such as data states, fault and compensation handling. We also propose a big-step operational semantics which incorporates all these key features. Our verification rules are proven sound with respect to this underlying semantics. The application of the verification rules is illustrated via the proof search process for a nontrivial example.

References

1. Thatte S. XLANG: web service for business process design. Microsoft, 2001 2. Leymann F. WSFL: web service flow language. http://www-4.ibm.com/software/solutions/webservices/pdf/WSFL.pdf,IBM, 2001 3. Butler M, Ferreira C . An operational semanticsfor StAC, a language for modelling long-running business transactions. In: Proceedings of the 6th International Conferenceon Coordination Models and Languages, Lecture Notes in Computer Science,Vol 2949, Springer, 2004, 87–104 4. Alves A, Arkin A, Askary S, et al.. web service business process execution languageversion 2.0. http://docs.oasis-open. org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html,OASIS Standard, 2007 5. Barreto C, Bullard V, Erl T, et al.. web service business process execution languageversion 2.0 primer. OASIS Standard, 2007 6. Qiu Z, Wang S, Pu G et al.. Semantics of bpel4ws-likefault and compensation handing. In: Proceedingsof the 1st International Symposium of Formal Methods Europe, LectureNotes in Computer Science, Vol 3582, Springer, 2005, 350–365 7. Pu G, Zhu H, Qiu Z et al.. Theoretical foundationof scope-based compensable flow language for web service. In: Proceedings of the 1st International Conferenceon Formal Methods for Open Object-Based Distributed Systems, LectureNotes in Computer Science, Vol 4037, Springer, 2006, 251–266 8. Qiu Z, Zhao X, Cai C et al.. Towards the theoreticalfoundation of choreography. In: Proceedingsof the 6th International World Wide Web Conference, ACM Press, 2007, 973–982 9. He J, Zhu H, Pu G . A model for bpel-like languages. Frontiers of Computer Science in China. 2007, 1(1):9–19. doi:10.1007/s11704-007-0002-7 10. Zhu H, He J, Li J et al.. Algebraic approachto linking the semantics of web services. In: Proceedings of the 5th IEEE International Conference on SoftwareEngineering and Formal Method, 2007, 315–328 11. Xu Q, de Roever W P, He J . The rely-guarantee method for verifying shared variableconcurrent programs. Formal Aspects ofComputing, 1997, 9(2): 149–174. doi:10.1007/BF01211617 12. Zhu H . Linkingthe semantics of a multithreaded discrete event simulation language.Dissertation for the Doctoral Degree. LondonSouth Bank University, 2005 13. Fowler M, Scott K . UML distilled: a brief guideto the standard object modeling language. Addison-Wesley, 2000 14. Garcia-Molina H, Salem K . Sagas. In: Proceedings of the Association for Computing Machinery Special InterestGroup on Management of Data Conference, ACM Press, 1987, 249–259 15. Moss J . Nestedtransactions: an approach to reliable distributed computing. Dissertationfor the Doctoral Degree. MassachusettsInstitute of Technology, 1981 16. Analst W, Dumas M, Hofstede A, et al.. Analysis of web services composition languages:the case of bpel4ws. In: Proceedings ofthe 22nd International Conference on Conceptual Modeling, LectureNotes in Computer Science, Vol 2813. Springer, 2003, 200–215 17. Hamadi R, Benatallah B . A petri net-based model forweb service composition. In: Proceedingsof the 14th Australasian Database Conference, Vol 47, Adelaide, Australia, 2003, 191–200 18. Brogi A, Canal C, Pimentel E et al.. Formalizing web servicechoreographies. Electronic Notes in TheoreticalComputer Science, 2004, 105: 73–94. doi:10.1016/j.entcs.2004.05.007 19. Andrews T, Curbera F, Dholakia H, et al.. Business process execution language for webservices 1.1. 2003 20. Bruni R, Melgratti H, Montanari U . Theoretical foundations for compensations in flow compositionlanguages. In: Proceedings of the 32ndSIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL),New York, USA, 2005, 209–220 21. Duan Z, Bernstein A, Lewis P et al.. Semantics based verificationand synthesis of bpel4ws abstract processes. In: Proceedings of the IEEE International Conference on Web Services, 2004, 734–737 22. Duan Z, Bernstein A, Lewis P et al.. A model for abstractprocess specification, verification and composition. In: Proceedings of the 2nd International Conference on Service OrientedComputing, New York, USA, 2004, 232–241 23. Fu X, Bultan T, Su J . Analysis of interacting bpel web services.In: Proceedings of the 13th International World WideWeb Conference, ACM Press, 2004, 621–630 24. Holzmann G . Thespin model checker:primer and reference manual. Addison-Wesley, 2003 25. Pu G, Zhao S, Wang S . Towards the semantics and verification of bpel4ws. In: Proceedings of the International Workshop onWeb Languages and Formal Methods (WLFM), Electronic Notes in TheoreticalComputer Science, Vol 151, Elsevier, 2005, 33–52 26. Bengtsson J, Larsen K, Larsson F, et al.. Uppaal-a tool suitable for automatic verificationof real-time systems. In: Proceedings ofthe DIMACS/SYCON Workshop on Hybrid Systems III: Verification andControl, Secaucus, New Jersey, USA, New York: Springer, 1996, 232–243