Abstract
Web service choreography languages provide a way to describe the collaboration protocol of multiple services that exchange information in order to achieve a common goal. This description may be seen as a specification that should be respected by the joint behavior of the set of services implementing the choreography. Such a conformance requires that (i) the observable behavior of the implementation corresponds to the behavior described by the protocol specification, and (ii) the business information is properly managed, guaranteeing that the participants have a shared knowledge about it, according to what is specified in the choreography. In this paper we present a choreography conformance analysis approach that addresses both the behavioral correspondence and the business information management. The key features of the approach are the capability to deal with asynchronous interactions and the ability to model and analyse the data managed and exchanged in the protocol, thus providing more accurate verification results. We also present symbolic techniques based on these formalizations that can be used for model checking of the choreography conformance.
This work is partially funded by the MIUR-FIRB project RBNE0195K5, “KLASE”, by the MIUR-PRIN 2004 project “STRAP”, and by the EU-IST project FP6-016004 “SENSORIA”.
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
Andrews, T., Curbera, F., Dolakia, H., Goland, J., Klein, J., Leymann, F., Liu, K., Roller, D., Smith, D., Thatte, S., Trickovic, I., Weeravarana, S.: Business Process Execution Language for Web Services (version 1.1) (2003)
OMG: Business Process Modeling Language (BPML) (2005), http://www.bpmi.org
W3C (Web Services Choreography Description Language Version 1.0. W3C Candidate Recommendation, November 9, 2005), http://www.w3.org/TR/ws-cdl-10/
Kazhamiakin, R., Pistore, M., Santuari, L.: Analysis of Communication Models in Web Service Compositions. In: Proc. WWW 2006 (2006)
Dijkman, R.M., Dumas, M.: Service-Oriented Design: A Multi-Viewpoint Approach. Int. J. Cooperative Inf. Syst. 13(4), 337–368 (2004)
Guerin, F., Pitt, J.: Verification and compliance testing. In: Communication in Multiagent Systems, pp. 98–112 (2003)
Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Choreography and orchestration: A synergic approach for system design. In: Benatallah, B., Casati, F., Traverso, P. (eds.) ICSOC 2005. LNCS, vol. 3826, pp. 228–240. Springer, Heidelberg (2005)
Graf, S., Saidi, H.: Construction of abstract state graph with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. In: Proc. FMSD 2004 (2004)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (1990)
Clarke, E., Emerson, E., Sistla, A.: Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2) (1986)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C.: Verifying the Conformance of Web Services to Global Interaction Protocols: a First Step. In: Proc. EPEW/WS-FM (2005)
Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-Based Analysis of Obligations in Web Service Choreography. In: Proc. AICT-ICIW 2006 (2006)
van der Aalst, W.M., Dumas, M., Ouyang, C., Rozinat, A., Verbeek, H.: Choreography Conformance Checking: An Approach based on BPEL and Petri Nets. Technical report, BPM Center Report BPM-05-25 (2005)
Brogi, A., Canal, C., Pimentel, E., Vallecillo, A.: Formalizing Web Services Choreographies. In: Proc. WS-FM 2004. ENTCS (2004)
Bravetti, M., Guidi, C., Lucchi, R., Zavattaro, G.: Supporting e-commerce systems formalization with choreography languages. In: Preneel, B., Tavares, S. (eds.) SAC 2005. LNCS, vol. 3897. Springer, Heidelberg (2006)
Carbone, M., Honda, K., Yoshida, N.: A theoretical basis of communication-centred concurrent programming (2005), http://lists.w3.org/Archives/Public/public-ws-chor/2005Nov/att-0015/part1_Nov25.pdf
Fu, X., Bultan, T., Su, J.: Synchronizability of Conversations among Web Services. IEEE Transactions on Software Engineering 31(12), 1042–1055 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kazhamiakin, R., Pistore, M. (2006). Choreography Conformance Analysis: Asynchronous Communications and Information Alignment. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds) Web Services and Formal Methods. WS-FM 2006. Lecture Notes in Computer Science, vol 4184. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11841197_15
Download citation
DOI: https://doi.org/10.1007/11841197_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-38862-3
Online ISBN: 978-3-540-38865-4
eBook Packages: Computer ScienceComputer Science (R0)