Choice, interoperability, and conformance in interaction protocols and service choreographies

ABSTRACT

Many real-world applications of multiagent systems require independently designed (heterogeneous) and operated (autonomous) agents to interoperate. We consider agents who offer business services and collaborate in interesting business service engagements. We formalize notions of interoperability and conformance, which appropriately support agent heterogeneity and autonomy. With respect to autonomy, our approach considers the choices that each agent has, and how their choices are coordinated so that at any time one agent leads and its counterpart follows, but with initiative fluidly shifting among the participants. With respect to heterogeneity, we characterize the variations in the agents' designs, and show how an agent may conform to a specification or substitute for another agent. Our approach addresses a challenging problem with multi-party interactions that existing approaches cannot solve. Further, we introduce a set of edit operations by which to modify an agent design so as to ensure its conformance with others.

REFERENCES

• 1: Unified Modeling Language: Superstructure, version 2.0, 2004.
• 2: Marco Alberti , Davide Daolio , Paolo Torroni , Marco Gavanelli , Evelina Lamma , Paola Mello, Specification and verification of agent interaction protocols in a logic-based system, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus [doi>10.1145/967900.967918]
• 3: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman , Moshe Y. Vardi, Alternating Refinement Relations, Proceedings of the 9th International Conference on Concurrency Theory, p.163-178, September 08-11, 1998
• 4: Lacramioara Astefanoaei , Frank S. de Boer, Model-checking agent refinement, Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems, May 12-16, 2008, Estoril, Portugal
• 5: M. Baldoni, C. Baroglio, A. Martelli, and V. Patti. A priori conformance verification for guaranteeing interoperability in open environments. In Proc. of ICSOC 2006, LNCS 4294, pages 339--351. Springer, 2006.
• 6: M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and C. Schifanella. Verifying protocol conformance for logic-based communicating agents. In Proc. of CLIMA V, number 3487 in LNCS, pages 192--212. Springer, 2005.
• 7: D. Berardi, D. Calvanese, G. De Giacomo, M. Lenzerini, and M. Mecella. Automatic composition of e-services that export their behavior. In Proc. of Int. Conf. on Service-Oriented Computing, ICSOC'03, LNCS, pages 43--58. Springer, 2003.
• 8: L. Bordeaux, G. Salaün, D. Berardi, and M. Mecella. When are two web services compatible? In TES 2004, volume 3324 of LNCS, pages 15--28. Springer, 2005.
• 9: M. Bravetti and G. Zavattaro. Contract based multi-party service composition. In FSEN, volume 4767 of LNCS, pages 207--222. Springer, 2007.
• 10: M. Bravetti and G. Zavattaro. A theory for strong service compliance. In COORDINATION, volume 4467 of LNCS, pages 96--112. Springer, 2007.
• 11: Tevfik Bultan , Xiang Fu , Richard Hull , Jianwen Su, Conversation specification: a new approach to design and analysis of e-service composition, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary [doi>10.1145/775152.775210]
• 12: S. Carpineti, G. Castagna, C. Laneve, and L. Padovani. A formal account of contracts for web services. In WS-FM, volume 4184 of LNCS, pages 148--162. Springer, 2006.
• 13: A. K. Chopra and M. P. Singh. Interoperation in protocol enactment. In Declarative Agent Languages and Technologies V, volume 4897 of LNCS, pages 36--49, 2008.
• 14: Luca de Alfaro , Thomas A. Henzinger, Interface Theories for Component-Based Design, Proceedings of the First International Workshop on Embedded Software, p.148-165, October 08-10, 2001
• 15: Nirmit V. Desai , Munindar P. Singh, Interorganizational business interactions: contracts, processes, evolution, North Carolina State University, 2008
• 16: Nirmit Desai , Ashok U. Mallya , Amit K. Chopra , Munindar P. Singh, Interaction Protocols as Design Abstractions for Business Processes, IEEE Transactions on Software Engineering, v.31 n.12, p.1015-1027, December 2005 [doi>10.1109/TSE.2005.140]
• 17: Howard Foster , Sebastian Uchitel , Jeff Magee , Jeff Kramer, Model-Based Analysis of Obligations in Web Service Choreography, Proceedings of the Advanced Int'l Conference on Telecommunications and Int'l Conference on Internet and Web Applications and Services, p.149, February 19-25, 2006
• 18: C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof. Stuck-free conformance. In CAV, volume 3114 of LNCS, pages 242--254. Springer, 2004.
• 19: Laura Giordano , Alberto Martelli, Verifying Agent Conformance with Protocols Specified in a Temporal Action Logic, Proceedings of the 10th Congress of the Italian Association for Artificial Intelligence on AI*IA 2007: Artificial Intelligence and Human-Oriented Computing, September 10-13, 2007, Rome, Italy [doi>10.1007/978-3-540-74782-6_14]
• 20: N. Guermouche, O. Perrin, and C. Ringeissen. Timed Specification For Web Services Compatibility Analysis. In Proc. of Int. Workshop on Automated Specification and Verification of Web Systems, WWV'07, 2007.
• 21: Alessio Lomuscio , Hongyang Qu , Monika Solanki, Towards verifying compliance in agent-based web service compositions, Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems, May 12-16, 2008, Estoril, Portugal
• 22: Tim Miller , Peter McBurney, Annotation and matching of first-class agent interaction protocols, Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems, May 12-16, 2008, Estoril, Portugal
• 23: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 24: Frantisek Plasil , Stanislav Visnovsky, Behavior Protocols for Software Components, IEEE Transactions on Software Engineering, v.28 n.11, p.1056-1076, November 2002 [doi>10.1109/TSE.2002.1049404]
• 25: Sriram K. Rajamani , Jakob Rehof, Conformance Checking for Models of Asynchronous Message Passing Software, Proceedings of the 14th International Conference on Computer Aided Verification, p.166-179, July 27-31, 2002
• 26: M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proc. of LICS, Symposium on Logic in Computer Science, pages 332--344. IEEE Computer Society, 1986.
• 27: Daniel M. Yellin , Robert E. Strom, Protocol specifications and component adaptors, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.292-333, March 1997 [doi>10.1145/244795.244801]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.5 On-line Information Services

General Terms:
Design, Theory, Verification

Keywords:
choreographies, conformance, interaction protocols, interoperability, web services