133
Views
2
CrossRef citations to date
0
Altmetric
Section A

The semantics and verification of timed service choreography

, , , &
Pages 384-402 | Received 20 Aug 2012, Accepted 02 Apr 2013, Published online: 24 May 2013

References

  • G. Behrmann, A. David, and K. Larsen, A tutorial on UPPAAL, in International School on Formal Methods for the Design of Computer, Communication, and Software Systems, M. Bernardo and F. Corradini, eds., Vol. 3185 of Lecture Notes in Computer Science, Springer-Verlag, Bertinora, Italy, 2004, pp. 200–236.
  • A. Brogi, C. Canal, E. Pimentel, and A. Vallecillo, Formalizing web service choreographies, Electron. Notes Theor. Comput. Sci. 105 (2004), pp. 73–94. doi: 10.1016/j.entcs.2004.05.007
  • R. Bruni, M.J. Butler, C. Ferreira, C.A.R. Hoare, H.C. Melgratti, and U. Montanari, Comparing two approaches to compensable flow composition, in CONCUR: Concurrency Theory, M. Abadi and L. de Alfaro, eds., Proceedings of 16th International Conference, CONCUR 2005, San Francisco, CA, August 23–26, LNCS, Vol. 3653, Springer, Heidelberg, 2005, pp. 383–397.
  • R. Bruni, H.C. Melgratti, and U. Montanari, Theoretical foundations for compensations in flow composition languages, in Proceedings of POPL 2005, 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Long Beach, CA, January 12–14, J. Palsberg and M. Abadi, eds., ACM Press, New York, 2005, pp. 209–220.
  • N. Busi, R. Gorrieri, C. Guidi, R. Lucchi, and G. Zavattaro, Choreography and orchestration conformance for system design, in Coordination, P. Ciancarini and H. Wiklicky, eds., Vol. 4038 of Lecture Notes in Computer Science, Springer, Bologna, Italy, 2006, pp. 63–81.
  • M.-E. Cambronero, G.D. Ruiz, V. Valero, and E. Martínez, Validation and verification of web services choreographies by using timed automata, J. Log. Algebr. Program. 80(1) (2011), pp. 25–49. doi: 10.1016/j.jlap.2010.02.001
  • M. Carbone, K. Honda, and N. Yoshida, A theoretical basis of communication-centres concurrent programming, First International Summer School on Emerging Trends in Concurrency (TIC'06), Bertinoro, Italy, 2006.
  • J. Davis, Specification and Proof in Real-Time CSP, Cambridge University Press, Cambridge, 1993.
  • N. Guermouche and C. Godart, Characterizing compatibility of timed choreography, Int. J. Web Serv. Res. (JWSR’11) 8 (2011), pp. 1–28. doi: 10.4018/jwsr.2011040101
  • R. Hamadi and B. Benatallah, A petri net-based model for web service compostion, Proceedings of the 14th Australasian Database Conference, Vol. 17, Australian Computer Society, Darlinghurst, Australia, 2003, pp. 191–200.
  • J. He, H. Zhu, and G. Pu, A model for BPEL-like languages. Front. Comput. Sci. China 1(1) (2007), pp. 9–19. doi: 10.1007/s11704-007-0002-7
  • C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall International, Hemel Hempstead, Herts, 1985.
  • G.J. Holzmann, Parallelizing the spin model checker, in Model Checking Software, Alastair F. Donaldson and David Parker, eds., 19th International Workshop, SPIN 2012, Oxford, UK, July 23–24, Springer, Heidelberg, 2012, pp. 155–171.
  • D. Kitchin, W.R. Cook, and J. Misra, A language for task orchestration and its semantic properties, in Concur 2006 – Concurrency Theory, Christel Baier and Holger Hermanns, eds., Proceedings of 17th International Conference, CONCUR 2006, Bonn, Germany, August 27–30, Lecture Notes in Computer Science, Springer, Heidelberg, August 2006, pp. 477–491.
  • D. Kitchin, A. Quark, W.R. Cook, and J. Misra. The Orc programming language, in FMOODS/FORTE 2009: 11th Formal Methods for Open Object-Based Distributed Systems and 29th Formal Techniques for Networked and Distributed Systems, D. Lee, A. Lopes and A. Poetzsch-Heffter, eds., Lecture Notes in Computer Science, Springer, Lisboa, Portugal 2009, pp. 1–25.
  • Y. Liu, Model checking concurrent and real-time systems: The PAT approach, Ph.D. thesis, National University of Singapore, 2009.
  • Y. Liu, J. Sun, and J. S. Dong, Pat 3: An extensible architecture for building multidomain model checkers, ISSRE: IEEE 22nd International Symposium on Software Reliability Engineering, Hiroshima, Japan, 2011, pp. 190–199.
  • OASIS web services business process execution language (WSBPEL). Available at http://www.oasis-open.org/committees/tc_home.php?wg_abbrev=wsbpel
  • On-the-fly, LTL model checking with SPIN. Available at http://spinroot.com/
  • Process analysis toolkit (PAT). Available at http://www.comp.nus.edu.sg/ pat/
  • L. Peng, C. Cai, Z. Qiu, and G. Pu, Verification of channel passing in choreography with model checking, SOCA: IEEE International Conference on Service-Oriented Computing and Applications, Taipei, Taiwan, 2009, pp. 1–5.
  • G. Pu, H. Zhu, Z. Qiu, S. Wang, X. Zhao, and J. He, Theoretical foundations of scopebased compensable flow language for web service, in Formal Methods for Open Object-Based Distributed Systems, R. Gorrieri and H. Wehrheim, eds., Proceedings of 8th IFIP WG 6.1 International Conference, FMOODS 2006, Bologna, Italy, June 14–16, Vol. 4037 of Lecture Notes in Computer Science, Springer, Heidelberg, 2006, pp. 251–266.
  • G. Pu, Y. Zhao, Z. Wang, L. Feng, H. Zhu, and J. He, A denotational model for web services choreography, in Distributed Computing and Internet Technology, M. Parashar and S. K. Aggarwal, eds., 5th International Conference, ICDCIT 2008, New Delhi, India, December 10–12, Vol. 5375 of Lecture Notes in Computer Science, Springer, Heidelberg, 2008, pp. 1–12.
  • Z. Qiu, S. Wang, G. Pu, and X. Zhao. Semantics of BPEL4WS-like fault and compensation handling, in FM 2005: Formal Methods, J. Fitzgerald, I.J. Hayes, and A. Tarlecki, eds., Proceedings of International Symposium of Formal Methods Europe, Newcastle, UK, July 18–22, Vol. 3582 of Lecture Notes in Computer Science, Springer, Heidelberg, 2005, pp. 350–365.
  • G.M. Reed and A.W. Roscoe, A timed model for communicating sequential processes, in ICALP: International Colloquium Automata, Languages and Programming, Rennes, France, Laurent Kott, ed., Vol. 226 of Lecture Notes in Computer Science, Springer, Heidelberg, 1986, pp. 314–323.
  • G.M. Reed and A.W. Roscoe, The timed failures-stability model for CSP, Theor. Comput. Sci. 211(1–2) (1999), pp. 85–127. doi: 10.1016/S0304-3975(98)00214-X
  • A.W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall International Series in Computer Science, Hemel Hempstead, Herts, 1997.
  • A.W. Roscoe, Understanding Concurrent Systems, Vol. 211, Springer-Verlag, New York, 2010.
  • S. Schneider, An operational semantics for timed CSP, Inf. Comput. 116(2) (1995), pp. 193–213. doi: 10.1006/inco.1995.1014
  • J. Sun, Y. Liu, and J.S. Dong, Model checking csp revisited: Introducing a process analysis toolkit, in ISoLA: Leveraging Applications of Formal Methods, Verification and Validation, Tiziana Margaria and Bernhard Steffen, eds., Third International Symposium, Porto Sani, Greece, 2008, pp. 307–322.
  • J. Sun, Y. Liu, J.S. Dong, and C. Chen, Integrating specification and programs for system modeling and verification, TASE: Third IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, 2009, pp. 127–135.
  • J. Sun, Y. Liu, J.S. Dong, and X. Zhang, Verifying stateful timed CSP using implicit clocks and zone abstraction, in International Conference on Formal Engineering Methods, Rio de Janeiro, Brazil, K. Breitman and A. Cavalcanti, eds., Vol. 5885 of Lecture Notes in Computer Science, Springer, Heidelberg, 2009, pp. 581–600.
  • UPPAAL. Design verification for embedded systems. Available at http://www.uppaal.com/
  • Web service choreography interface (WSCI) 1.0. Available at http://www.w3.org/TR/wsci/
  • Web services choreography description language, version 1.0. Available at http://www.w3.org/TR/ws-cdl-10/
  • Web services flow language (WSFL). Available at http://xml.coverpages.org/wsfl.html
  • Xlang. Web services for business process design. Available at http://www.xml.com/pub/r/1153
  • H. Yang, X. Zhao, C. Cai, and Z. Qiu, Exploring the connection of choreography and orchestration with exception handling and finalization/compensation, in IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems, Tallinn, Estonia, J. Derrick and J. Vain, eds., Vol. 4574 of Lecture Notes in Computer Science, Springer, Heidelberg, 2007, pp. 81–96.
  • H. Yang, X. Zhao, C. Cai, and Z. Qiu, Model-checking of web services choreography, in International Symposium on Service Oriented System Engineering, Jhongli, Taiwan, J. Lee, D. Liang, and Y. C. Cheng, eds., IEEE Computer Society, Washington, DC, 2008, pp. 79–84.
  • Y. Zhao, Z. Wang, G. Pu, and H. Zhu, A formal model for service choreography with exception hangling and finalization, in International Symposium on Theoretical Aspects of Software Engineering Conference, Taipei, Taiwan, F. Wang and H.-C.Y. Qin, eds., IEEE Computer Society, Washington, DC, 2010, pp. 15–24.
  • H. Zhu, J. He, G. Pu, and J. Li, An operational approach to BPEL-like programming, SEW: 31st Annual IEEE / NASA Software Engineering Workshop, Loyola College, Columbia, MD, 2007, pp. 236–245.

Reprints and Corporate Permissions

Please note: Selecting permissions does not provide access to the full text of the article, please see our help page How do I view content?

To request a reprint or corporate permissions for this article, please click on the relevant link below:

Academic Permissions

Please note: Selecting permissions does not provide access to the full text of the article, please see our help page How do I view content?

Obtain permissions instantly via Rightslink by clicking on the button below:

If you are unable to obtain permissions via Rightslink, please complete and submit this Permissions form. For more information, please visit our Permissions help page.