Modeling and Verifying Agent-Based Communities of Web Services

Communities of web) services are virtual spaces that can dynamically gather different web services having complementary functionabties in order to provide composite services In the last two years, some approaches have been proposed using multi-agent systems to organize communities of web services This trend has increased the flexibility but also the system complexity The system becomes hard to check by simply inspecting its model Therefore. model checking, which is a well-established formal technique for verifying, communication and cooperation in multi-agent, systems, is used in this paper to verify the system correctness in terms of satisfying desirable properties The approach presented in the paper is used to verify communities of web services modeled in UML, activity diagram We first, translate the activity diagram into ail interpreted system model using predefined transformation rules Specifications are expressed as formulae in a logic extending the Computation Tree Logic CTL- with agent commitments needed for their communication Then, both the model and formulae are used as inputs for the multi-agent symbolic model checker MCMAS We illustrate out approach with a short case study, in which we show how communication properties of simulated communities are verified