Semantic Web Services的自动化组合技术

论文摘要

本论文以Semantic Web Services（语义Web服务）的自动化组合技术为研究的中心,围绕这一主要问题,分3个部分分别分析与探讨了服务的语义、组合服务、以及自动化服务组合的方法。本论文所有的研究,都是基于服务的语义进行的。“语义”是Semantic Web Services体系中最重要的一个部分。服务被解释成一种特殊的软件组件,提取其输入参数（（?）nput）、输出参数（（?）utput）、前置条件（（?）recondition）、执行效果（（?）ffect）、以及执行功能（IO-（?）inculum）这5个要素,即（I,O,P,E,V）,给出了服务作为一个整体的语义定义。以此语义定义为基础,分析了服务语义之间的关联关系,给出了“服务语义匹配”的严格的形式化定义。对服务组合演算的产物——组合服务,做了深入的分析。组合服务是一种服务执行流程,以π-Calculus为形式化描述工具,分别以数据流模型（DFM）和中心控制点模型（CCM）为视点,定义了两种表达形式。定义了基于DFM表述形式的组合服务语义积分算法（SCA）,用于从组件服务的语义以及组合模型来获取组合服务的语义,这是服务验证的基础。定义了基于CCM表述形式的BPEL脚本生成规则（CCM2BPEL）,用于获取可发布执行的组合服务最终形式。给出了从DFM模型到CCM模型的映射算法（DFM2CCM）。以“证明与程序的等价理论（Proof as Programs）”为依据,以“基于推理的程序生成技术（Deductive Program Synthesis）”为原型,给出了实现自动化服务组合的技术解决方案——基于逻辑定理证明的自动化服务组合技术。依照一个逻辑公式转换模板,把服务的语义（I,O,P,E,V）映射成一个一阶谓词逻辑（First-Order Logic,FOL）定理,以已有服务作为已知定理,目标服务作为待证明定理。从OWL本体库以及背景知识库中导入相关的外部语义知识,以弥合已知定理之间的语义缝隙。应用自动化定理证明引擎（Automatic Theorem Prover,ATP）,获取证明结果,提取证明路径。最后利用CSEA算法,从证明路径中提取目标服务的实现体（基于DFM模型）,从而构建了完整的从需求到最终结果的技术路径（Problem→Proof→DFM→CCM→BPEL）。这种“从证明到程序”的方法,保证了所得组合结果的完备性与正确性。通过一个完整的应用示例,对论文中的各个关键步骤进行了具体的说明与演示。实现了一个原型系统,用于对整套方法进行初步的可行性验证。

论文目录

• 摘要
• ABSTRACT
• 第1章 绪论
• 1.1 引言
• 1.1.1 网络的发展
• 1.1.2 Semantic Web
• 1.1.3 Services
• 1.1.4 Service-Oriented Architecture
• 1.1.5 Services与Intelligent Agents
• 1.2 本论文所要解决的问题
• 1.3 问题的解决方案概述
• 1.3.1 研究路径
• 1.3.2 服务组合与软件生成
• 1.3.3 问题的核心解决方案
• 1.4 本论文的主要贡献
• 1.5 本论文的结构和安排
• 1.6 本章参考文献
• 第2章 Web Services及其组合
• 2.1 Web Services相关规范介绍
• 2.1.1 Web Services系统架构
• 2.1.2 WSDL
• 2.1.3 OWL-S
• 2.1.4 BPEL
• 2.2 Web Services的自动化组合
• 2.2.1 基于AI Planning技术的
• 2.2.2 基于Program Synthesis技术的
• 2.3 本章小结
• 2.4 本章参考文献
• 第3章 Semantic Web Services的语义
• 3.1 描述Semantic Web Services语义的五个要素
• 3.2 服务的语义
• 3.3 服务上层本体
• 3.4 应用示例:小镇信息查询
• 3.5 服务语义之间的关联
• 3.5.1 语义闭包（Semantic Closure）
• 3.5.2 服务语义的匹配、强匹配、等价
• 3.5.3 匹配服务的副作用
• 3.5.4 语义匹配、等价的逻辑判定法
• 3.6 服务演算的语义含义
• 3.6.1 原子服务与组合服务
• 3.6.2 服务发现
• 3.6.3 服务替换
• 3.6.4 服务组合
• 3.6.5 服务验证
• 3.7 本章小结
• 3.8 本章参考文献
• 第4章 组合服务
• 4.1 组合服务的表达
• 4.1.1 进程代数——Process Algebra
• 4.1.2 π-Calculus
• 4.1.3 π-Calculus vs.λ-Calculus
• 4.1.4 基于π-Calculus的组合服务表达方式
• 4.2 组合服务的语义
• 4.2.1 组合服务的语义演算算法:SCA
• 4.2.2 SCA算法解释
• 4.2.3 SCA算法的应用示例
• 4.2.4 服务验证过程示例
• 4.3 基于中心控制点的组合服务进程模型
• 4.3.1 数据流模型（DFM）与中心控制点模型（CCM）
• 4.3.2 模型转换算法:DFM2CCM
• 4.3.3 DFM2CCM算法解释
• 4.3.4 转换算法应用示例
• 4.4 BPEL脚本的生成
• 4.4.1 从中心控制点模型到BPEL脚本的映射:CCM2BPEL
• 4.4.2 BPEL脚本生成示例
• 4.5 本章小结
• 4.6 本章参考文献
• 第5章 自动化服务组合技术
• 5.1 基于逻辑定理证明的程序生成技术
• 5.1.1 程序的自动化生成技术
• 5.1.2 Otter自动定理证明系统介绍
• 5.2 服务的自动化组合
• 5.2.1 形式化表示:服务语义的逻辑转化
• 5.2.2 逻辑证明:在系统中使用自动证明引擎
• 5.2.3 程序提取算法（CSEA）:获取目标服务的实现体
• 5.3 应用示例:小镇信息查询
• 5.3.1 所有的已有服务
• 5.3.2 本体库导入过程
• 5.3.3 语义信息输入到Otter证明引擎
• 5.3.4 目标服务实现体的提取过程
• 5.4 原型系统介绍
• 5.4.1 简介
• 5.4.2 运行示例
• 5.5 本章小结
• 5.6 本章参考文献
• 第6章 总结
• 6.1 对目标问题的解决情况
• 6.1.1 对"问题1"的回答
• 6.1.2 对"问题2"的回答
• 6.1.3 对"问题3"的回答
• 6.1.4 对"问题4"的回答
• 6.1.5 对核心问题的回答
• 6.2 未来设想
• 6.3 本章参考文献
• 附录 致谢
• 附录 作者在攻读博士期间发表的学术论文