基于时间自动机的Web服务模型检测

传统的基于有限状态机的组合Web服务模型检测方法不能保证带有时间约束的组合Web服务的正确性.把组合Web服务看成多智能体系统,将带有时间约束的Web服务智能体建模为时间自动机,通过并发组合构成时间自动机网络,从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟,并验证其活性、安全性和死锁等性质.采用该方法对雇员出差安排组合Web服务进行建模和验证,结果表明,该组合Web服务存在死锁问题.最后通过分析死锁产生的路径,完善该组合Web服务的通信协议,从而消除了死锁.

Model Checking Web Services Based on Timed Automata

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