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

Warda El Kholy, Jamal Bentahar, Mohamed El Menshawy, Hongyang Qu, Rachida Dssouli

Research output: Contribution to journalArticlepeer-review

23 Scopus citations


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.

Original languageBritish English
Pages (from-to)7478-7494
Number of pages17
JournalExpert Systems with Applications
Issue number16
StatePublished - 15 Nov 2014


  • Agent-based web services
  • Commitment protocols
  • Conditional commitments
  • Multi-agent systems
  • Symbolic model checking
  • Verification


Dive into the research topics of 'Modeling and verifying choreographed multi-agent-based web service compositions regulated by commitment protocols'. Together they form a unique fingerprint.

Cite this