Reachability analysis of web service compositions via NWA  

使用NWA对组合web服务进行可达性分析(英文)

作　　者：杜旭涛[1] 邢春晓[2] 周立柱[1] 

机构地区：[1]清华大学计算机科学与技术系,北京100084 [2]清华大学信息技术研究院

出　　处：《Journal of Southeast University(English Edition)》2008年第3期293-295,共3页东南大学学报（英文版）

基　　金：The National Key Technology R&D Program of Chinaduring the 11th Five-Year Plan Period(No.2006BAH02A12);the National High Technology Research and Development Program of China(863 Program)(No.2006AA010101)

摘　　要：In order to improve the design and implementation quality of web service compositions,formal methods are used to model them and certain properties are verified.WCFA （web service interface control flow automata）is used to model web services,especially the control flow and possible interactions with other web services.A web service composition consists of a set of interacting WCFA.The global behavior of web service compositions is captured by NWA（nested word automata）.A variation of the depth-first search algorithm is used to transform a set of WCFA into an NWA.State formulae and call stacks at each node of NWA are computed by a path-sensitive reachability analysis.Safety properties,call stack inspection properties and pre/post-conditions of service invocations are described by assertions.Then verification of these assertions is carried out by an automated SAT tool.为了提高组合web服务的设计和实现质量,使用形式化方法对其进行建模并对其关键性质进行验证.使用web服务接口控制流自动机(WCFA)对web服务进行建模,主要描述其控制流及与其他web服务的交互关系.组合web服务由一组交互的WCFA组成.使用嵌套字自动机(NWA)对组合web服务的整体行为进行建模.将一组WCFA转换为嵌套字自动机(NWA)的算法是深度优先搜索算法的变种,算法中使用路径相关的可达性分析计算NWA的每个节点的状态公式和调用栈.安全性相关性质、调用栈相关性质及服务调用的前置和后置条件都可以用断言来描述,然后使用一个自动的可满足性(SAT)求解工具对这些断言进行验证.

关 键 词：web service composition FORMALISM nested word automata （NWA） web service interface control flow automata （WCFA） VERIFICATION 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]