关键词: 模型检测，Web服务，时间自动机，UPPAAL

Abstract: The traditional model checking technictues based on finite state automaton cannot guarantee the correctness of Web services composition with timed constraints. We regarded Web services composition as multi agent system Each atomic Web service was modeled as timed automaton and by parallel composition of them,a network of timed automata was generated and inputted into the model checker UPPAAL. By using the proposed method and UPPAAL we were able to simulate the execution process and verify the liveness,safety and deadlock properties of a Web services composi- tion. We took the atomic services of employee evection arrangements service as a case study of the proposed method and verified some related liveness and safety properties. A deadlock problem of the case study was found by simulation. By analyzing the execution path leading to the deadlock state, we found the reason and finally eliminated the deadlock by revising the communication protocol of the Web services composition.L

Key words: Model checking, Web Services, Timed Automata, UPPAA