This Article 
 Bibliographic References 
 Add to: 
An Integrated Workbench for Model-Based Engineering of Service Compositions
April-June 2010 (vol. 3 no. 2)
pp. 131-144
Howard Foster, Imperial College London, London
Sebastian Uchitel, Imperial College London, London
Jeff Magee, Imperial College London, London
Jeff Kramer, Imperial College London, London
The Service-Oriented Architecture (SOA) approach to building systems of application and middleware components promotes the use of reusable services with a core focus of service interactions, obligations, and context. Although services technically relieve the difficulties of specific technology dependency, the difficulties in building reusable components is still prominent and a challenge to service engineers. Engineering the behavior of these services means ensuring that the interactions and obligations are correct and consistent with policies set out to guide partners in building the correct sequences of interactions to support the functions of one or more services. Hence, checking the suitability of service behavior is complex, particularly when dealing with a composition of services and concurrent interactions. How can we rigorously check implementations of service compositions? What are the semantics of service compositions? How does deployment configuration affect service composition behavior safety? To facilitate service engineers designing and implementing suitable and safe service compositions, we present in this paper an approach to consider different viewpoints of service composition behavior analysis. The contribution of the paper is threefold. First, we model service orchestration, choreography behavior, and service orchestration deployment through formal semantics applied to service behavior and configuration descriptions. Second, we define types of analysis and properties of interest for checking service models of orchestrations, choreography, and deployment. Third, we describe mechanical support by providing a comprehensive integrated workbench for the verification and validation of service compositions.

[1] A. Alves et al., "Web Service Business Execution Language (WS-BPEL) v2.0," OASIS, OASIS Standard, http://docs.oasis-open. org/wsbpel/2.0/OS wsbpel-v2.0-OS.html, Apr. 2007.
[2] N. Kavantzas, D. Burdett, G. Ritzinger, T. Fletcher, and Y. Lafon, "Web Services Choreography Description Language Version 1.0," W3C, W3C Candidate Recommendation,, Nov. 2005.
[3] R. Akkiraju, H. Flaxer, H. Chang, T. Chao, L.J. Zhang, F. Wu, and J.J. Jeng, "A Framework for Facilitating Dynamic e-Business via Web Services," Proc. Workshop Object-Oriented Web Services at ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '01), 2001.
[4] D. Booth and D.H. Haas, "Web Services Architecture (WS-A)," World Wide Web Consortium (W3C), Working Group Note,, Feb. 2004.
[5] I. Pyarali, M. Spivak, R. Cytron, and C.S. Douglas, "Evaluating and Optimizing Thread Pool Strategies for Real-Time CORBA," Proc. ACM SIGPLAN Workshop Languages, Compilers and Tools for Embedded Systems, 2001.
[6] J. Magee, N. Dulay, S. Eisenbach, and J. Kramer, "Specifying Distributed Software Architectures," Proc. Fifth European Software Eng. Conf. (ESEC '95), 1995.
[7] OMG, "Unified Modelling Language (UML) 2.1.1," Object Management Group, Specification,, Feb. 2007.
[8] R. Milner, Communication and Concurrency. Prentice-Hall, 1989.
[9] J. Magee, J. Kramer, and D. Giannakopoulou, "Analysing the Behaviour of Distributed Software Architectures: A Case Study," Proc. Fifth IEEE Workshop Future Trends of Distributed Computing Systems, 1997.
[10] J. Magee and J. Kramer, Concurrency—State Models and Java Programs, second ed. John Wiley, 2006.
[11] J. Magee, "FSP Language Specification,", 2009.
[12] ITU-T-Z20, "Formal Description Techniques (FDT) Message Sequence Chart (MSC) (Z20)," Int'l Telecomm. Union, Telecomm. Standardisation Sector, ITU-T Recommendation, http://www. languagesZ120.pdf, Apr. 2004.
[13] S. Uchitel, J. Kramer, and J. Magee, "Synthesis of Behavioral Models from Scenarios," IEEE Trans. Software Eng., vol. 29, no. 2, pp. 99-115, Feb. 2003.
[14] H. Foster, S. Uchitel, J. Magee, J. Kramer, and M. Hu, "Using a Rigorous Approach for Engineering Web Service Compositions: A Case Study," Proc. Services Computing Conf. (SCC '05), 2005.
[15] W. Emmerich, B. Butchart, L. Chen, B. Wassermann, and S.L. Price, "Grid Service Orchestration Using the Business Process Execution Language (BPEL)," J. Grid Computing, vol. 3, nos. 3/4, pp. 283-304, , 2005.
[16] H. Foster, S. Uchitel, J. Magee, and J. Kramer, "WS-Engineer: A Tool for Model-Based Verification of Web Service Compositions and Choreography," Proc. Int'l Conf. Software Eng. (ICSE '06), 2006.
[17] M. Papazoglou and J. Yang, "Design Methodology for Web Services and Business Processes, Technologies for E-Services," Lecture Notes in Computer Science, Springer-Verlag, 2002.
[18] T. Gardner, "UML Modelling of Automated Business Process with Mapping to BPEL4WS," Proc. First European Workshop Object Orientation and Web Services (EOOWS '03), 2003.
[19] S. Iyengar, "Business Process Integration Using UML and BPEL4WS," Proc. XML Conf. and Exposition (XML '03), 2003.
[20] K. Mantell, "From UML to BPEL," technical report, IBM DeveloperWorks, 2003.
[21] S. Woodman and E.D. Palmer, "Notations for the Specification and Verification of Composite Web Services," Proc. Eighth IEEE Int'l Enterprise Distributed Object Computing (EDOC), 2004.
[22] M. Pistore and A.M. Roveri, "Requirements-Driven Verification of Web Services," Proc. Int'l Workshop Web Services and Formal Methods (WS-FM '04), 2004.
[23] E. Yu, "Towards Modeling and Reasoning Support for Early Requirements Engineering," Proc. Third Int'l Symp. Requirements Eng. (RE '97), 1997.
[24] R. Hamadi and B. Benatallah, "A Petri Net-Based Model for Web Services Composition," Proc. Third IEEE Int'l Conf. Web Services (ICWS), 2004.
[25] X. Yi and K.J. Kochut, "Towards Efficient Integration of Complex Web Services Using a Unified Model for Protocol and Process," Proc. Fifth Int'l Conf. Internet Computing (IC '04), 2004.
[26] X. Yi and K. Kochut, "Process Composition of Web Services with Complex Conversation Protocols: A Colored Petri Nets Based Approach," Proc. Design, Analysis, and Simulation of Distributed Systems Symp. (DASD '04), 2004.
[27] S. Nakajima, "Model-Checking Verification for Reliable Web Service," Proc. Workshop Object-Oriented Web Services at ACM SIGPLAN Conf. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2002.
[28] F. Leymann, "Web Services Flow Language Specification (WSFL 1.0)," technical report, IBM, 2001.
[29] S. Nakajima, "On Verifying Web Service Flows," Proc. Int'l Symp. Applications and the Internet (SAINT '02), 2002.
[30] A. Ferrara, "Web Services: A Process Algebra Approach," Proc. Second Int'l Conf. Service Oriented Computing (ICSOC '04), 2004.
[31] G. Salaun and A. Ferrara, "Negotiation among Web Services Using LOTOS/CADP," Proc. European Conf. Web Services (ECWS '04), 2004.
[32] D. Bianculli, C. Ghezzi, and P. Spoletini, "A Model Checking Approach to Verify BPEL4WS Workflows," Proc. Int'l Conf. Service-Oriented Computing and Applications (SOCA '07), 2007.
[33] H. Foster, "Architecture and Behaviour Analysis for Engineering Service Modes," Proc. Second Workshop Principles of Eng. Service Oriented Systems (PESOS '09), May 2009.

Index Terms:
Service-oriented architecture, composite services, services models, Web services modeling, analysis, validation.
Howard Foster, Sebastian Uchitel, Jeff Magee, Jeff Kramer, "An Integrated Workbench for Model-Based Engineering of Service Compositions," IEEE Transactions on Services Computing, vol. 3, no. 2, pp. 131-144, April-June 2010, doi:10.1109/TSC.2010.19
Usage of this product signifies your acceptance of the Terms of Use.