Abstract
Web services choreography as an important approach of composing web services describes the global model of service interactions among a set of participants. Modern software design paradigms promote hierarchy as one of the key constructs for structuring complex specifications. In development of complex service-oriented systems, hierarchical composition in which a composed service could also be composed into a high level system model is a great approach for system modeling, and behavioural equivalence which checks whether two choreographies in different levels describe essentially the same behaviour is an important aspect of system verification. This paper proposes a formal modeling and analysis approach for hierarchical web services choreographies. A formal language Chor which originates from WS-CDL describes dynamic behaviour of choreographies and a novel bisimulation is used for analyzing behavioural equivalence of Chor language. We introduce a hierarchical model for describing and analyzing complex choreographies. Abstract choreographies can be refined to detailed models and external and observable behaviour be preserved equivalently. Our approach can also be extended to formally analyze hierarchical and global interaction models for general concurrent systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Papazoglou, M.P., Traverso, P., Dustdar, S., Leymann, F.: Service-oriented computing: State of the art and research challenges. Computer 40(11), 38–45 (2007)
Peltz, C.: Web services orchestration and choreography. Computer 36(10), 46–52 (2003)
Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y., Barreto, C.: Web services choreography description language version 1.0. World Wide Web Consortium, Candidate Recommendation CR-ws-cdl-10-20051109 (November 2005)
Carbone, M., Yoshida, K.H.N., Milner, R., Brown, G., Ross-talbot, S.: A theoretical basis of communication-centred concurrent programming. Technical report (2006)
Milner, R.: Communicating and mobile systems: the pi-calculus, 5th edn. Cambridge University Press, Cambridge (2004)
Hoare, C.A.R.: Communicating sequential processes. Communication of ACM 21(8), 666–677 (1978)
Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the theoretical foundation of choreography. In: WWW 2007: Proceedings of the 16th International Conference on World Wide Web, pp. 973–982. ACM, New York (2007)
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)
Carbone, M., Honda, K., Yoshida, N.: Theoretical aspects of communication-centred programming. Electr. Notes Theor. Comput. Sci. 209, 125–133 (2008)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)
Guidi, C., Lucchi, R.: Formalizing mobility in service oriented computing. Journal of Software 2(1), 1–13 (2007)
Li, J., He, J., Zhu, H., Pu, G.: Modeling and verifying web services choreography using process algebra. In: SEW 2007: Proceedings of the 31st IEEE Software Engineering Workshop, pp. 256–268. IEEE Computer Society, Washington, DC (2007)
Yang, H., Zhao, X., Cai, C., Qiu, Z.: Model-checking of web services choreography. In: SOSE 2008: Proceedings of the 2008 IEEE International Symposium on Service-Oriented System Engineering, pp. 79–84. IEEE Computer Society, Washington, DC (2008)
Bultan, T., Ferguson, C., Fu, X.: A tool for choreography analysis using collaboration diagrams. In: ICWS 2009: Proceedings of the 2009 IEEE International Conference on Web Services, pp. 856–863. IEEE Computer Society, Washington, DC (2009)
Holzmann, G.: Spin model checker, the: primer and reference manual. Addison-Wesley Professional, Reading (2003)
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)
Li, J., Zhu, H., Pu, G.: Conformance validation between choreography and orchestration. In: TASE 2007: Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, pp. 473–482. IEEE Computer Society, Washington, DC (2007)
Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhao, Y., Li, J., Li, Z., Ma, D. (2011). Towards Hierarchical Modeling and Analysis of Web Services Choreography. In: Snene, M., Ralyté, J., Morin, JH. (eds) Exploring Services Science. IESS 2011. Lecture Notes in Business Information Processing, vol 82. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21547-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-21547-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21546-9
Online ISBN: 978-3-642-21547-6
eBook Packages: Computer ScienceComputer Science (R0)