Abstract
Global choreographies define the rules that peers should respect in their interaction, with the aim of guaranteeing interoperability. An abstract choreography can be seen as a protocol specification; it does not refer to specific peers and, especially in an open application domain, it might be necessary to retrieve a set of web services that fit in it. A crucial issue, that is raising attention, is verifying whether the business process of some peers, in particular the parts that encode the communicative behavior, will produce interactions which are conformant to the agreed protocol (legality issue). Such issue is tackled by the so called conformance test, which is a means for certifying the capability of interacting of the involved parts: two peers that are proved conformant to a same protocol will actually interoperate by producing a legal conversation. This work proposes an approach to the verification of a priori conformance of a business process to a protocol, which is based on the theory of formal languages and guarantees the interoperability of peers that are individually proved conformant.
This research is partially supported by MIUR Cofin 2003 “Logic-based development and verification of multi-agent systems” national project and by the European Commission and by the Swiss Federal Office for Education and Science within the 6th Framework Programme project REWERSE number 506779.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Specification and verification of agent interactions using social integrity constraints. In: Proc. of the Workshop on Logic and Communication in Multi-Agent Systems, LCMAS 2003, Eindhoven, the Netherlands, vol. 85(2). Elsevier, Amsterdam (2003)
Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services. Springer, Heidelberg (2004)
Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C.: Verifying protocol conformance for logic-based communicating agents. In: Leite, J., Torroni, P. (eds.) CLIMA 2004. LNCS (LNAI), vol. 3487, pp. 196–212. Springer, Heidelberg (2005)
Barros, A., Dumas, M., Oaks, P.: A critical overview of the web services choreography description language(ws-cdl). Business Process Trends (2005), http://www.bptrends.com
Berardi, D., Calvanese, D., De Giacomo, G.G., Lenzerini, M., Mecella, M.: Automatic composition of e-services that export their behavior. In: Orlowska, M.E., Weerawarana, S., Papazoglou, M.P., Yang, J. (eds.) ICSOC 2003. LNCS, vol. 2910, pp. 43–58. Springer, Heidelberg (2003)
BPEL4WS (2003), http://www-106.ibm.com/developerworks/library/ws-bpel
Bravetti, M., Guidi, C., Lucchi, R., Zavattaro, G.: Supporting e.commerce systems formalization with choreography languages. In: Proc. of SAC 2005. ACM Press, New York (2005)
Bultan, T., Fu, X., Hull, R., Su, J.: Conversation specification: A new approach to design and analysis of e-service composition. In: Proc. of WWW 2003 (2003)
Endriss, U., Maudet, N., Sadri, F., Toni, F.: Protocol conformance for logic-based agents. In: Proc. of IJCAI-2003, pp. 679–684 (2003)
Endriss, U., Maudet, N., Sadri, F., Toni, F.: Logic-based agent communication protocols. In: Dignum, F.P.M. (ed.) ACL 2003. LNCS (LNAI), vol. 2922, pp. 91–107. Springer, Heidelberg (2004)
Garg, V., Ragunath, M.T.: Concurrent regular expressions and their relationship to Petri nets. Theoretical Computer Science 96, 285–304 (1992)
Guerin, F., Pitt, J.: Verification and Compliance Testing. In: Huget, M.-P. (ed.) Communication in Multiagent Systems. LNCS (LNAI), vol. 2650, pp. 98–112. Springer, Heidelberg (2003)
Hopcroft, J.E., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Company, Reading (1979)
Huget, M.P., Koning, J.L.: Interaction Protocol Engineering. In: Huget, M.-P. (ed.) Communication in Multiagent Systems. LNCS (LNAI), vol. 2650, pp. 179–193. Springer, Heidelberg (2003)
Kavantzas, N., Burdett, D., Ritzinger, G., Lafon, Y.: Web services choreography description language version 1.0 (2004), Available at, http://www.w3.org/TR/ws-cdl-10
Mazzara, M., Lucchi, R.: A framework for generic error handling in business processes. In: Proc. of WS-FM 2004. ENTCS, vol. 105. Elsevier, Amsterdam (2004)
Odell, J., Parunak, H.V.D., Bauer, B.: Extending UML for agents. In: Proc. of the Agent-Oriented Information System Workshop at AAAI (2000)
Viroli, M.: Towards a formal foundation to orchestration languages. In: Proc. of WS-FM 2004, Eindhoven, the Netherlands. ENTCS, vol. 105, pp. 51–71. Elsevier, Amsterdam (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C. (2005). Verifying the Conformance of Web Services to Global Interaction Protocols: A First Step. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds) Formal Techniques for Computer Systems and Business Processes. EPEW WS-FM 2005 2005. Lecture Notes in Computer Science, vol 3670. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11549970_19
Download citation
DOI: https://doi.org/10.1007/11549970_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28701-8
Online ISBN: 978-3-540-31903-0
eBook Packages: Computer ScienceComputer Science (R0)