| 使用NWA对组合web服务进行可达性分析(英文) | |
| 杜旭涛 ; 邢春晓 ; 周立柱 ; Du Xutao ; Xing Chunxiao ; Zhou Lizhu | |
| 2010-05-12 ; 2010-05-12 | |
| 关键词 | 组合web服务 形式化方法 嵌套字自动机 web服务接口控制流自动机 验证 web service composition formalism nested word automata (NWA) web service interface control flow automata (WCFA) verification TP393.09 |
| 其他题名 | Reachability analysis of web service compositions via NWA |
| 中文摘要 | 为了提高组合web服务的设计和实现质量,使用形式化方法对其进行建模并对其关键性质进行验证.使用web服务接口控制流自动机(WCFA)对web服务进行建模,主要描述其控制流及与其他web服务的交互关系.组合web服务由一组交互的WCFA组成.使用嵌套字自动机(NWA)对组合web服务的整体行为进行建模.将一组WCFA转换为嵌套字自动机(NWA)的算法是深度优先搜索算法的变种,算法中使用路径相关的可达性分析计算NWA的每个节点的状态公式和调用栈.安全性相关性质、调用栈相关性质及服务调用的前置和后置条件都可以用断言来描述,然后使用一个自动的可满足性(SAT)求解工具对这些断言进行验证.; 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. |
| 语种 | 英语 ; 英语 |
| 内容类型 | 期刊论文 |
| 源URL | [http://hdl.handle.net/123456789/28381]  |
| 专题 | 清华大学 |
| 推荐引用方式 GB/T 7714 | 杜旭涛,邢春晓,周立柱,等. 使用NWA对组合web服务进行可达性分析(英文)[J],2010, 2010. |
| APA | 杜旭涛,邢春晓,周立柱,Du Xutao,Xing Chunxiao,&Zhou Lizhu.(2010).使用NWA对组合web服务进行可达性分析(英文).. |
| MLA | 杜旭涛,et al."使用NWA对组合web服务进行可达性分析(英文)".(2010). |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论