一种基于扩展有限自动机验证组合Web服务的方法  

An Extended Deterministic Finite Automata Based Method for the Verification of Composite Web Services

作　　者：雷丽晖[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,陕西西安710071

出　　处：《软件学报》2007年第12期2980-2990,共11页Journal of Software

基　　金：Supported by the National Natural Science Foundation of China under Grant Nos.60373103;60433010(国家自然科学基金);the Defence Pre-Research Project under Grant No.51315050105(装备预先研究项目)

摘　　要：为简化并自动化组合Web服务验证提出一种基于扩展有限自动机(extended deterministic finite automata,简称EDFA)验证组合Web服务的方法.使用EDFA可以准确地描述Web服务:EDFA的状态表达Web服务在与用户交互的过程中维护的状态;EDFA的状态转移及其标注描述Web服务与用户间的消息交换.EDFA给出Web服务交互过程的所有消息交换序列,刻画出Web服务的动态行为.使用基于EDFA的组合Web服务验证方法不但可以验证组合Web服务是否满足系统需求,还可以验证组合Web服务运行过程是否有逻辑错误与其他方法相比,该方法更适于验证开放式环境下的组合Web服务.To simplify and automate the verification of composite Web services, a method based on extended deterministic finite automata （EDFA） is presented. EDFA can describe Web services in an accurate way： the nodes represent states maintained by a service during the interactions between the service and its clientsi the state transitions represent message exchanges between the service and its clients. Therefore, the automaton depicts the temporal sequences of messages, i.e. the behavior of the service. With the EDFA-based method for the verification of composite Web services, whether the capabilities of a service meet system requirements and whether there exist logic errors in the interactions between a service and its clients can be verified. Compared with other methods, this method is more suitable for the verification of composite Web services in an open environment.

关 键 词：组合WEB服务 确定有限自动机 形式化验证 

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