Modeling and verifying choreographed multi-agent-based web service compositions regulated by commitment protocols

• Modeling multi-agent based web services using commitment protocols formalized as guarded automata with certain variables.
• Defining formal semantics for conditional commitments and associated actions for agent communication.
• Introducing a formal specification language of commitment protocols.
• Developing a symbolic model checking algorithm for the verification of web services composition.
• Computing the space complexity of the developed algorithm.

The competency to compose web services from available services is one of the most crucial problems in the paradigm of service-oriented computing. 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 multi-agent based web services, which offer high-level abstractions that support autonomy, business-level compliance, and flexible dynamic changes. In this article, we model interactions among multi-agent based web services by commitment modalities in the form of contractual obligations and devote multi-agent commitment protocols to regulate such interactions and engineer services composition. We develop and fully implement an automatic verifier 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. We analyze the time and space complexity of the verifier. Finally, we present the experimental results of two case studies, adopted to check the verifier’s efficiency and scalability.