Abstract: In order to solve the problem that analyzing the composite services by manual is rather difficult and time-consuming, an approach was proposed to verify composite services by model checking based on uMSD. How to represent the temporal properties of the composite service easily and intuitively is a critical issue of the approach. Because uMSD finds a balance between simplicity of use and expressiveness, the paper defined the formal syntax and semantics of uMSD. In the paper, uMSD was used to graphically represent the temporal properties of a composite service On-the-Job Assistant as a case study, presenting the feasibility of uMSI).A series of experiments show the approach can effectively detect the logical errors in the composite service.

Key words: Modal sequence diagram, Web service composition, Model checking