Verifying Multiagent-Based Web Service Compositions Regulated by Commitment Protocols

The ability to compose web services from available services is one of the most crucial problems in the service-oriented computing paradigm. Conventional software engineering approaches and even standard languages compose web services as workflow models that control the business logic required to coordinate data over participating services. Such models would not apply to the design of multiagent-based web services, which offer high-level abstractions that support autonomy, business-level compliance, and flexible dynamic changes. In this paper, we model interactions among multiagent-based services by commitment modalities in the figure of contractual obligations and devote multiagent commitment protocols to regulate such interactions and engineer services composition. We develop and fully implement a symbolic model checking algorithm by enriching the MCMAS model checker with certain symbolic algorithms to verify the correctness of protocols, given properties expressed in a temporal commitment logic, suitably extended with actions. The time complexity and space complexity of the developed algorithm are P-complete for explicit models and for PSPACE-complete concurrent programs. Finally, we report the experimental results of two case studies, adopted to check the algorithm´s efficiency.