The semantics and verification of timed service choreography

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.
   Google Scholar
• 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
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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
   Web of Science ®Google Scholar
• 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.
   Google Scholar
• J. Davis, Specification and Proof in Real-Time CSP, Cambridge University Press, Cambridge, 1993.
   Google Scholar
• 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
   Web of Science ®Google Scholar
• 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.
   Google Scholar
• 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
   Google Scholar
• C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall International, Hemel Hempstead, Herts, 1985.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• Y. Liu, Model checking concurrent and real-time systems: The PAT approach, Ph.D. thesis, National University of Singapore, 2009.
   Google Scholar
• 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.
   Google Scholar
• OASIS web services business process execution language (WSBPEL). Available at http://www.oasis-open.org/committees/tc_home.php?wg_abbrev=wsbpel
   Google Scholar
• On-the-fly, LTL model checking with SPIN. Available at http://spinroot.com/
   Google Scholar
• Process analysis toolkit (PAT). Available at http://www.comp.nus.edu.sg/ pat/
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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
   Web of Science ®Google Scholar
• A.W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall International Series in Computer Science, Hemel Hempstead, Herts, 1997.
   Google Scholar
• A.W. Roscoe, Understanding Concurrent Systems, Vol. 211, Springer-Verlag, New York, 2010.
   Google Scholar
• S. Schneider, An operational semantics for timed CSP, Inf. Comput. 116(2) (1995), pp. 193–213. doi: 10.1006/inco.1995.1014
   Web of Science ®Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• UPPAAL. Design verification for embedded systems. Available at http://www.uppaal.com/
   Google Scholar
• Web service choreography interface (WSCI) 1.0. Available at http://www.w3.org/TR/wsci/
   Google Scholar
• Web services choreography description language, version 1.0. Available at http://www.w3.org/TR/ws-cdl-10/
   Google Scholar
• Web services flow language (WSFL). Available at http://xml.coverpages.org/wsfl.html
   Google Scholar
• Xlang. Web services for business process design. Available at http://www.xml.com/pub/r/1153
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar
• 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.
   Google Scholar