The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - Third Quarter (2012 vol.5)
pp: 290-304
Gwen Salaün , Grenoble INP, INRIA, Grenoble
Tevfik Bultan , University of California, Santa Barbara, Santa Barbara
Nima Roohi , Sharif University of Technology, Tehran
ABSTRACT
Service-oriented computing has emerged as a new software development paradigm that enables implementation of Web accessible software systems that are composed of distributed services which interact with each other via exchanging messages. Modeling and analysis of interactions among services is a crucial problem in this domain. Interactions among a set of services that participate in a service composition can be described from a global point of view as a choreography. Choreographies can be specified using specification languages such as Web Services Choreography Description Language (WS-CDL) and visualized using graphical formalisms such as collaboration diagrams. In this paper, we present an encoding of collaboration diagrams into the LOTOS process algebra for choreography analysis. This encoding allows us to 1) check the temporal properties of choreographies using a LOTOS verification tool set called the Construction and Analysis of Distributed Processes (CADP) toolbox, 2) check the realizability of choreographies for both synchronous communication and bounded asynchronous communication, and 3) automate the peer generation process. Realizability indicates whether peers can be generated from a given choreography specification in such a way that the interactions of the generated peers exactly match the choreography specification. If a collaboration diagram is unrealizable, our approach extends the peer generation process by adding extra communication that guarantees that the peers behave according to the choreography specification.
INDEX TERMS
Collaboration, Message systems, Synchronization, Encoding, Asynchronous communication, Semantics, Availability, tools., Service protocols, choreography, realizability, process algebra, asynchronous communication, verification
CITATION
Gwen Salaün, Tevfik Bultan, Nima Roohi, "Realizability of Choreographies Using Process Algebra Encodings", IEEE Transactions on Services Computing, vol.5, no. 3, pp. 290-304, Third Quarter 2012, doi:10.1109/TSC.2011.9
REFERENCES
[1] X. Fu, T. Bultan, and J. Su, "Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services," Theoretical Computer Science, vol. 328, nos. 1/2, pp. 19-37, 2004.
[2] T. Bultan and X. Fu, "Specification of Realizable Service Conversations Using Collaboration Diagrams," Service Oriented Computing and Applications, vol. 2, no. 1, pp. 27-39, 2008.
[3] G. Salaün, L. Bordeaux, and M. Schaerf, "Describing and Reasoning on Web Services Using Process Algebra," Proc. IEEE Int'l Conf. Web Services (ICWS'04), pp. 43-51, 2004.
[4] W.M.P. van der Aalst, M. Dumas, C. Ouyang, A. Rozinat, and H.M.W. Verbeek, "Choreography Conformance Checking: An Approach Based on BPEL and Petri Nets," Proc. Dagstuhl Seminar on the Role of Business Processes in Service Oriented Architectures, 2006.
[5] X. Fu, T. Bultan, and J. Su, "Synchronizability of Conversations among Web Services," IEEE Trans. Software Eng., vol. 31, no. 12, pp. 1042-1055, Dec. 2005.
[6] R. Kazhamiakin and M. Pistore, "Analysis of Realizability Conditions for Web Service Choreographies," Proc. 26th Int'l Conf. Formal Techniques for Networked and Distributed Systems (FORTE '06), pp. 61-76, 2006.
[7] Z. Qiu, X. Zhao, C. Cai, and H. Yang, "Towards the Theoretical Foundation of Choreography," Proc. 16th Int'l Conf. World Wide Web (WWW '07), pp. 973-982, 2007.
[8] M. Carbone, K. Honda, and N. Yoshida, "Structured Communication-Centred Programming for Web Services," Proc. 16th European Conf. Programming (ESOP '07), pp. 2-17, 2007.
[9] H. Garavel, R. Mateescu, F. Lang, and W. Serwe, "CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes," Proc. 19th Int'l Conf. Computer Aided Verification (CAV '07), pp. 158-163, 2007.
[10] G.J. Holzmann, "The Model Checker SPIN," IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[11] G. Salaün and T. Bultan, "Realizability of Choreographies Using Process Algebra Encodings," Proc. Seventh Int'l Conf. Integrated Formal Methods (IFM '09), pp. 167-182, 2009.
[12] ISO, "LOTOS—A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour," Technical Report 8807, Int'l Standards Organisation, 1989.
[13] H. Garavel and F. Lang, "SVL: A Scripting Language for Compositional Verification," Proc. 21st Int'l Conf. Formal Techniques for Networked and Distributed Systems (FORTE '01), pp. 377-394, 2001.
[14] R. Mateescu and M. Sighireanu, "Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus," Science of Computer Programming, Special Issue on Formal Methods for Industrial Critical Systems, vol. 46, no. 3, pp. 255-281, 2003.
[15] R. Alur, K. Etessami, and M. Yannakakis, "Realizability and Verification of MSC Graphs," Theoretical Computer Science, vol. 331, no. 1, pp. 97-114, 2005.
[16] R. Milner, Communication and Concurrency, International Series in Computer Science. Prentice Hall, 1989.
[17] N. Busi, R. Gorrieri, C. Guidi, R. Lucchi, and G. Zavattaro, "Choreography and Orchestration Conformance for System Design," Proc. Eighth Int'l Conf. Coordination Models and Languages (Coordination '06), pp. 63-81, 2006.
[18] J. Li, H. Zhu, and G. Pu, "Conformance Validation between Choreography and Orchestration," Proc. First Joint IEEE/IFIP Symp. Theoretical Aspects of Software Eng. (TASE '07), pp. 473-482, 2007.
[19] J.M. Zaha, M. Dumas, A.H.M. ter Hofstede, A.P. Barros, and G. Decker, "Service Interaction Modeling: Bridging Global and Local Views," Proc. IEEE 10th Int'l Enterprise Distributed Object Computing Conference (EDOC '06), pp. 45-55, 2006.
[20] J. Mendling and M. Hafner, "From Inter-Organizational Workflows to Process Execution: Generating BPEL from WS-CDL," Proc. OTM Confederated Int'l Conf. Move to Meaningful Internet Systems (OTM '05), pp. 506-515, 2005.
[21] R. Alur, K. Etessami, and M. Yannakakis, "Inference of Message Sequence Charts," IEEE Trans. Software Eng., vol. 29, no. 7, pp. 623-633, July 2003.
[22] S. Uchitel, J. Kramer, and J. Magee, "Incremental Elaboration of Scenario-Based Specifications and Behavior Models Using Implied Scenarios," ACM Trans. Software Eng. and Methodology, vol. 1, no. 13, pp. 37-85, 2004.
[23] X. Fu, T. Bultan, and J. Su, "WSAT: A Tool for Formal Analysis of Web Services," Proc. Computer Aided Verification (CAV '04), pp. 510-514, 2004.
[24] N. Roohi, G. Salaün, and S.H. Mirian, "Analyzing Chor Specifications by Translation into FSP," Proc. Eighth Int'l Workshop Foundations of Coordination Languages and Software Architectures (FOCLASA '09), pp. 159-176, 2009.
[25] Pi4SOA Project, http:/www.pi4soa.org, 2012.
[26] R. Mateescu, P. Poizat, and G. Salaün, "Adaptation of Service Protocols Using Process Algebra and On-the-Fly Reduction Techniques," Proc. Sixth Int'l Conf. Service-Oriented Computing (ICSOC '08), pp. 84-99, 2008.
[27] A. Zisman, G. Spanoudakis, and J. Dooley, "A Framework for Dynamic Service Discovery," Proc. 23rd IEEE/ACM Int'l Conf. Automated Software Eng. (ASE '08), pp. 158-167, 2008.
[28] F. Duran, M. Ouederni., and G. Salaün, "Checking Protocol Compatibility Using Maude," Proc. Int'l Workshop Foundations of Coordination Languages and Software Architectures (FOCLASA '09), pp. 65-81, 2009.
[29] G. Salaün, "Generation of Service Wrapper Protocols from Choreography Specifications," Proc. IEEE Sixth Int'l Conf. Software Eng. and Formal Methods (SEFM '08), pp. 313-322, 2008.
28 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool