A Priori Conformance Verification for Guaranteeing Interoperability in Open Environments

  • Matteo Baldoni
  • Cristina Baroglio
  • Alberto Martelli
  • Viviana Patti
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4294)


An important issue, in open environments like the web, is guaranteeing the interoperability of a set of services. When the interaction scheme that the services should follow is given (e.g. as a choreography or as an interaction protocol), it becomes possible to verify, before the interaction takes place, if the interactive behavior of a service (e.g. a BPEL process specification) respects it. This verification is known as “conformance test”. Recently some attempts have been done for defining conformance tests w.r.t. a protocol but these approaches fail in capturing the very nature of interoperability, turning out to be too restrictive. In this work we give a representation of protocol, based on message exchange and on finite state automata, and we focus on those properties that are essential to the verification of the interoperability of a set of services. In particular, we define a conformance test that can guarantee, a priori, the interoperability of a set of services by verifying properties of the single service against the protocol. This is particularly relevant in open environments, where services are identified and composed on demand and dynamically, and the system as a whole cannot be analyzed.


Multiagent System Interaction Protocol Finite State Automaton Incoming Message Execution Context 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Montali, M.: An abductive framework for a-priori verification of web services. In: Principles and Practice of Declarative Programming, PPDP 2006. ACM Press, New York (2006)Google Scholar
  2. 2.
    Alberti, M., Daolio, D., Torroni, P., Gavanelli, M., Lamma, E., Mello, P.: Specification and verification of agent interaction protocols in a logic-based system. In: ACM SAC 2004, pp. 72–78. ACM, New York (2004)Google Scholar
  3. 3.
    Alonso, G., Casati, F., Kuno, H., Machiraju, V.: Web Services. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  4. 4.
    Arnold, A.: Finite Transition Systems. Pearson Education, London (1994)zbMATHGoogle Scholar
  5. 5.
    Baldoni, M., Baroglio, C., Martelli, A.: Verification of protocol conformance and agent interoperability. In: Toni, F., Torroni, P. (eds.) CLIMA 2005. LNCS (LNAI), vol. 3900, pp. 265–283. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Baldoni, M., Baroglio, C., Martelli, A., Patti, V.: Reasoning about interaction protocols for customizing web service selection and composition. J. of Logic and Algebraic Programming, special issue on Web Services and Formal Methods (2006) (to appear)Google Scholar
  7. 7.
    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, vol. 3487, pp. 192–212. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Baldoni, M., Baroglio, C., Martelli, A., Patti, V., Schifanella, C.: Verifying the conformance of web services to global interaction protocols: a first step. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) EPEW/WS-EM 2005. LNCS, vol. 3670, pp. 257–271. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Berardi, D., Giacomo, G.D., Lenzerini, M., Mecella, M., Calvanese, D.: Synthesis of underspecified composite -services based on automated reasoning. In: ICSOC, pp. 105–114 (2004)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Chopra, A.K., Singh, M.P.: Producing compliant interactions: Conformance, coverage, and interoperability. In: Baldoni, M., Endriss, U. (eds.) DALT 2006. LNCS (LNAI), vol. 4327, pp. 1–15. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Decker, G., Zaha, J.M., Dumas, M.: Execution semantics for service choreographies. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 163–177. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Foster, H., Uchitel, S., Magee, J., Kramer, J.: Model-based analysis of obligations in web service choreography. In: Proc. of IEEE International Conference on Internet & Web Applications and Services (2006)Google Scholar
  15. 15.
    van Glabbeek, R.J.: Bisimulation. In: Urban, J.E., Dasgupta, P. (eds.) Encyclopedia of Distributed Computing, Kluwer, Dordrecht (2000) available at, Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Heckel, B.: Thinking Java. Prentice Hall, Englewood Cliffs (2005)Google Scholar
  18. 18.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)Google Scholar
  19. 19.
    Kazhamiakin, R., Pistore, M.: Choreography conformance analysis: Asynchronous communications and information alignment. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 227–241. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  20. 20.
    Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing Interacting BPEL Processes. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 17–32. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  22. 22.
    OMG. Unified modeling language: Superstructure (2005)Google Scholar
  23. 23.
    van der Aalst, W.M.P.: Business alignment: Using process mining as a tool for delta analysis and conformance testing. Requirements Engineering Journal 10(3), 198–211 (2005)CrossRefGoogle Scholar
  24. 24.
    Zhao, X., Yang, H., Qui, Z.: Towards the formal model and verification of web service choreography description language. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 273–287. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Matteo Baldoni
    • 1
  • Cristina Baroglio
    • 1
  • Alberto Martelli
    • 1
  • Viviana Patti
    • 1
  1. 1.Dipartimento di InformaticaUniversità degli Studi di TorinoTorinoItaly

Personalised recommendations