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

• 作者: 周立柱 杜旭涛 邢春晓
• 来源期刊: 东南大学学报（英文版）
• 学科: 工学
• 关键词: 组合web服务 形式化方法 嵌套字自动机 web服务接口控制流自动机 验证
• 年，卷（期）: 2008,（3）
• 页码范围: 293-295
• 页数: 3页
• 分类号: TP311
• 字数: 491字
• 语种: 英文
• DOI: 10.3969/j.issn.1003-7985.2008.03.010

摘要

为了提高组合web服务的设计和实现质量,使用形式化方法对其进行建模并对其关键性质进行验证.使用web服务接口控制流自动机(WCFA)对web服务进行建模,主要描述其控制流及与其他web服务的交互关系.组合web服务由一组交互的WCFA组成.使用嵌套字自动机(NWA)对组合web服务的整体行为进行建模.将一组WCFA转换为嵌套字自动机(NWA)的算法是深度优先搜索算法的变种,算法中使用路径相关的可达性分析计算NWA的每个节点的状态公式和调用栈.安全性相关性质、调用栈相关性质及服务调用的前置和后置条件都可以用断言来描述,然后使用一个自动的可满足性(SAT)求解工具对这些断言进行验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周立柱	清华大学计算机科学与技术系	69	3313	19.0	57.0
2	邢春晓	清华大学信息技术研究院	84	2349	18.0	47.0
6	杜旭涛	清华大学计算机科学与技术系	1	1	1.0	1.0