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

Model Checking Web Services Based on Timed Automata

作　　者：骆翔宇[1,2] 轩爱成[1] 沙宗鲁[1] 

机构地区：[1]桂林电子科技大学计算机与控制学院,桂林541004 [2]清华大学软件学院,北京100084

出　　处：《计算机科学》2010年第8期139-142,197,共5页Computer Science

基　　金：国家自然科学基金(60763004);中国博士后科学基金(20090450389);广西青年科学基金(桂科青0728090);广西研究生教育创新计划项目(2008105950812M424)资助

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

关 键 词：模型检测 WEB服务 时间自动机 UPPAAL 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]