Abstract: Correctness verification of Web service composition plays an important role for improving software development efficiency and realizing service value-added. To study the correctness of Web service composition and their formal verification method from a high and abstract view, considering the real-time feature in Web service composition, based on the description of Web service composition using software architecture description language XYZ/ADL,the real-time description XYZ/RE was transformed to timed automata, the properties that the composite system should be satisfied were expressed in CTL formula, last, the correctness of Web service composition was automatically verified through a model checking tool-UPPAAL.

Key words: Web service composition, Model checking, XYZ/ADL, XYZ/RE, UPPAAL