| 使用NWA对组合web服务进行可达性分析 |
| |
| 引用本文： | 杜旭涛,邢春晓,周立柱.使用NWA对组合web服务进行可达性分析[J].东南大学学报,2008,24(3). |
| |
| 作者姓名： | 杜旭涛 邢春晓 周立柱 |
| |
| 作者单位： | [1]清华大学计算机科学与技术系,北京100084 [2]清华大学信息技术研究院,北京100084 [3]清华大学清华信息科学与技术国家实验室,北京100084 |
| |
| 基金项目： | National Key Technology R&D Program of China during the 11th Five-Year Plan Period，国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 为了提高组合web服务的设计和实现质量,使用形式化方法对其进行建模并对其关键性质进行验证.使用web服务接口控制流自动机（WCFA）对web服务进行建模,主要描述其控制流及与其他web服务的交互关系.组合web服务由一组交互的WCFA组成.使用嵌套字自动机（NWA）对组合web服务的整体行为进行建模.将一组WCFA转换为嵌套字自动机（NWA）的算法是深度优先搜索算法的变种,算法中使用路径相关的可达性分析计算NWA的每个节点的状态公式和调用栈.安全性相关性质、调用栈相关性质及服务调用的前置和后置条件都可以用断言来描述,然后使用一个自动的可满足性（SAT）求解工具对这些断言进行验证.
|
| 关 键 词： | 组合web服务 形式化方法 嵌套字自动机 web服务接口控制流自动机 验证 |
Reachability analysis of web service compositions via NWA |
| |
| Du Xutao,Xing Chunxiao,Zhou Lizhu.Reachability analysis of web service compositions via NWA[J].Journal of Southeast University(English Edition),2008,24(3). |
| |
| Authors: | Du Xutao Xing Chunxiao Zhou Lizhu |
| |
| Abstract: | 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. |
| |
| Keywords: | web service composition formalism nested word automata (NWA) web service interface control flow automata (WCFA) verification |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
