Abstract

This thesis includes two main contributions: the first one is specifying the use of argumentative agents in the design and development of communities of Web services; the second is using a formal technique to verify communication protocols against given properties for these communities. Web services that provide a similar functionality are gathered into a single community, independently of their origins, locations, and ways of doing. Associating Web services with argumentative agents that are able to persuade and negotiate with others organizes these Web services in a better way so that they can achieve the goals they set in an efficient way. A community is led by a master component, which is responsible among others for attracting new Web services to the community, retaining existing Web services in the community, and identifying the Web services in the community that will participate in composite scenarios. Besides FIPA-ACL, argumentative dialogue games are also used for agent interaction. In this thesis, we use tableau-based model checking algorithm to verify our argumentative agent-base community of Web services negotiation protocol. This algorithm aims at verifying systems designed as a set of autonomous interacting agents. We provide the soundness, completeness, termination and complexity results. We also simulate our specification with Jadex BDI programming language and implement our verification with a modified and enhanced version of CWB-NC model checker. Keywords. Multi-agent systems, BDI agent architecture, model checking, agent oriented programming, FIPA-ACL, dialogue game, agent-based negotiation protocol, Jadex, CWB-NC.