摘要: 本论文以Semantic Web Services(语义Web服务)的自动化组合技术为研究的中心，围绕这一主要问题，分3个部分分别分析与探讨了服务的语义、组合服务、以及自动化服务组合的方法。 本论文所有的研究，都是基于服务的语义进行的。“语义”是Semantic We... 展开 本论文以Semantic Web Services(语义Web服务)的自动化组合技术为研究的中心，围绕这一主要问题，分3个部分分别分析与探讨了服务的语义、组合服务、以及自动化服务组合的方法。 本论文所有的研究，都是基于服务的语义进行的。“语义”是Semantic Web Services体系中最重要的一个部分。服务被解释成一种特殊的软件组件，提取其输入参数((_I)nput)、输出参数((_O)utput)、前置条件((_P)recondition)、执行效果((_E)ffect)、以及执行功能(IO-（_V）inculum)这5个要素，即(I，O，P，E，V)，给出了服务作为一个整体的语义定义。以此语义定义为基础，分析了服务语义之间的关联关系，给出了“服务语义匹配”的严格的形式化定义。 对服务组合演算的产物—组合服务，做了深入的分析。组合服务是一种服务执行流程，以π-Calculus为形式化描述工具，分别以数据流模型(DFM)和中心控制点模型(CCM)为视点，定义了两种表达形式。定义了基于DFM表述形式的组合服务语义积分算法(SCA)，用于从组件服务的语义以及组合模型来获取组合服务的语义，这是服务验证的基础。定义了基于CCM表述形式的BPEL脚本生成规则(CCM2BPEL)，用于获取可发布执行的组合服务最终形式。给出了从DFM模型到CCM模型的映射算法(DFM2CCM)。 以“证明与程序的等价理论(Proofas 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)。这种“从证明到程序”的方法，保证了所得组合结果的完备性与正确性。 通过一个完整的应用示例，对论文中的各个关键步骤进行了具体的说明与演示。实现了一个原型系统，用于对整套方法进行初步的可行性验证。 收起