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

doi:10.1016/j.eswa.2014.05.046

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

2014-11-01

19

PRE

AI

DOI：10.1016/j.eswa.2014.05.046

原文链接

原文求助

摘要

En 中文

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. (C) 2014 Elsevier Ltd. All rights reserved.

Keyword:

Multi-agent systems

Conditional commitments

Commitment protocols

Agent-based web services

Symbolic model checking

Verification

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

摘要

AI总结

期刊

机构