|
|
|
Verifying BPEL-like programs with Hoare logic |
| LUO Chenguang1, QIN Shengchao1, QIU Zongyan2 |
| 1.Department of Computer Science, Durham University; 2.LMAM and Department of Informatics, School of Mathematical Sciences, Peking University; |
|
|
|
|
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.
|
|
Issue Date: 05 December 2008
|
|
| 1 |
Thatte S. XLANG: web service for business process design.http://www.gotdotnet.com/team/xml_wsspecs/xlang-c/default.htm, 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. http://docs. oasis-open.org/wsbpel/2.0/Primer/wsbpel-v2.0-Primer.html,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. http://download.boulder.ibm.com/ibmdl/pub/software/dw/specs/WS-bpel.pdf, 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
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
