Validation and verification of Web services choreographies by using timed automata

A. Ankolenkar et al., DAML-S: web service description for the semantic web, in: Proc. First International Semantic Web Conference, 2002, pp. 348–363. A. Arkin et al., Web Service Choreography Interface (WSCI) 1.0. <http:/www.w3.org/TR/wsci/>. A. Arkin et al., Web Services Business Process Execution Language Version 2.0, December 2004. <http://www.oasis-open.org/committees/download.php/10347/wsbpel-specification-draft-120204.htm>. R. Alur, D. Dill, Automata for modeling real-time systems, in: ICALP, 1990, pp. 322–335. Alur, 1994, A theory of timed automata, Theoret. Comput. Sci., 126, 183, 10.1016/0304-3975(94)90010-8 Bravetti, 2007, A theory for strong service compliance, vol. 4467, 96 Bravetti, 2008, Contract compliance and choreography conformance in the presence of message queues, vol. 5387 Brogi, 2004, Formalizing web service choreographies, Electron. Notes Theor. Comput. Sci., 105, 73, 10.1016/j.entcs.2004.05.007 Cambronero, 2009, A comparative study between WSCI, WS-CDL and OWL-S, 377 M.E. Cambronero, G. Díaz, E. Martínez, V. Valero, L. Tobarra, WST: a tool supporting timed composite web services model transformation, in: Simulation: Transactions of the Society for Modeling and Simulation International, in press. M. Carbone, K. Honda, N. Yoshida, A theoretical basis of communication-centres concurrent programming, in: First International Summer School on Emerging Trends in Concurrency (TIC’06), 2006. G. Díaz, J.J. Pardo, M.E. Cambronero, V. Valero, F. Cuartero, Verification of web services with timed automata, in: Proceedings of First International Workshop on Automated Specification and Verification of Web Sites, Electronic Notes in Theoretical Computer Science, vol. 1125, 157/2, 2005. Díaz, 2009, Automatically deriving choreography-conforming systems of services, 9 J.S. Dong, Y. Liu, J. Sun, X. Zhang, Verification of computation orchestration via timed automata, in: International Conference on Formal Engineering Methods (ICFEM), 2006, pp. 226–245. X. Du, C. Xing, L. Zhou, Z. Li, Nested web service interface control flow automata, in: Proc. 4th International Conference on Next Generation Web Services Practices, 2008, pp. 129–136. H. Foster, W. Emmerich, J. Kramer, J. Magee, D.S. Rosenblum, S. Uchitel, Model checking service compositions under resource constraints, in: ESEC/SIGSOFT FSE, 2007, pp. 225–234. R. Hamadi, B. Benatallah, A petri net-based model for web service composition, in: Proc. 14th Australasian Database Conference, vol. 17, 2003, pp. 191–200. K. Honda, N. Yoshida, M. Carbone, Multiparty asynchronous session types, in: POPL, 2008, pp. 273–284. Larsen, 1997, UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transfer, 1, 134, 10.1007/s100090050010 N. Lohmann, J. Kleine, Fully-automatic translation of open workflow net models into simple abstract bpel processes, in: Modellierung, 2008, pp. 57–72. Milner, 1989 Milner, 1992, A calculus of mobile processes, parts I and II, Inform. and Comput., 100, 1, 10.1016/0890-5401(92)90008-4 N. Kavantzas et al., Web Service Choreography Description Language (WSCDL) 1.0. <http://www.w3.org/TR/ws-cdl-10/>. S. Narayanan, S. Mcllraith, Simulation, verification and automated composition of web services, in: Proc. 11th International World Wide Conference, 2002, pp. 77–88. G. Salaün, L. Bordeaux, M. Schaerf, Describing and reasoning on web services using process algebra, in: Proc. 2nd International Conference on Web Services (ICWS), 2004, pp. 43–51. Sharygina, 2007, Model checking with abstraction for web services, 121 Valero, 2009, A petri net approach for the design and analysis of web services choreographies, J. Logic Algebraic Program., 78, 359, 10.1016/j.jlap.2008.09.002 W.M.P. van der Aalst, N. Lohmann, P. Massuthe, C. Stahl, K. Wolf, From public views to private views – correctness-by-design for services, in: WS-FM, 2007, pp. 139–153. H. Yang, X. Zhao, C. Cai, Z. Qiu, Model-checking of web services choreography, in: IEEE International Workshop on Service-Oriented System Engineering, 2008, pp. 79–84. W. L. Yeung, Mapping WS-CDL and BPEL into CSP for behavioural specification and verification of web services, in: European Conference on Web Services (ECOWS), 2006, pp. 297–305. Zhou, 2006, Pi4SOA: a policy infrastructure for verification and control of service collaboration, 307