PDF(261 KB)
Verifying BPEL-like programs with Hoare logic
- LUO Chenguang1, QIN Shengchao1, QIU Zongyan2
Author information
+
1.Department of Computer Science, Durham University; 2.LMAM and Department of Informatics, School of Mathematical Sciences, Peking University;
Show less
History
+
Published |
05 Dec 2008 |
Issue Date |
05 Dec 2008 |
{{custom_sec.title}}
{{custom_sec.title}}
{{custom_sec.content}}
This is a preview of subscription content, contact
us for subscripton.
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