Abstract During the last decade, software engineering community has witnessed the emerging of SOA architecture, where Web services play a crucial role. It prompts the concept of Web Service Composition (WSC). Even though interesting, this issue posed some remarkable challenges, one of which is constraint handling. To be more precise, one needs to ensure that the composite Web service fulfills, at the same time, many constraints, including functional constraints, Quality of Service (QoS), and the execution order of the component services, or temporal relations. Those constraints are of different natures, thus finding an efficient verification on all kinds of constraints during the composition process is by no means a trivial task. Backed by a solid foundation of temporal logic, model checking (MC) is a suitable approach to handle this issue. However, MC-based approach suffers from the infamous problem of state-space explosion, making it limited when applied to real-life situations. The work in this paper addresses the problem by proposing various approaches for handling the state-space exploration, including (i) an introduction of an LTS-based model known as LTS4WS, which can avoid generating full schema of Web service composition and allow on-the-fly verification on the state space; (ii) heuristics strategies to find the best potential composition, and (iii) a bitwise-based indexing mechanism for fast location of suitable Web services. All of those approaches are unified in a single tool, known as WSCOVER. As a result, a significant improvement of performance has been made, especially as compared with the other existing works in the same field.
展开▼
