题目：基于重写逻辑的OWL-S语义解释的研究与实现

软件模型对基于模型的测试以及可靠性分析等都有重要作用。软件模型的描述语言多种多样，其中OWL-S作为Web 服务描述方面的W3C推荐标准，有着通用性好、描述能力强、与Web服务结合紧密、相关资源丰富等优点。然而OWL-S也存在着一部分语义的描述不是形式化的缺点：OWL-S本体定义中，没有描述执行过程中的各种进程的原子性、执行方式、执行步骤，也没有描述控制结构和进程的各种属性如何影响组合进程的执行过程，而是在解释OWL-S的规范中用自然语言陈述了这些语义。我们把OWL-S的语义中表达动态行为的部分称之为动态语义，它同时包含了代数语义和操作语义。OWL-S的动态语义的非形式化性，导致无法深入分析OWL-S的描述。对OWL-S动态语义进行形式化描述，可以更有效的对OWL-S描述的软件结构中的控制流、数据流及其它内容进行深入的分析与检查。本论文在语言层面采用重写逻辑形式化地描述了OWL-S语义中非形式化的部分，并在此基础上设计并实现了一个自动转换工具。主要工作如下：（1） 使用重写逻辑形式化地定义了OWL-S语义中非形式化部分。本论文使用Maude形式化的描述了经过简化的OWL-S的动态语义和SWRL规则语言的语义，形成了OWL-S动态语义框架。以此框架为基础，对具体的OWL-S模型的转化工作仅涉及把OWL-S描述语法转化为Maude描述语法，模型的语义则已经由框架定义，与转换过程无关。（2） 提出了一种从OWL-S模型转换为Maude模型的方法。以第一部分的形式化描述工作完成的OWL-S语义框架为基础，研究了具体的模型从OWL-S语言向Maude语言转换的方法。该方法对OWL-S模型的IOPR、数据绑定、控制结构和进程主体等各个组成部分以及涉及的数据类型分别进行转换，并为进程构建一个模拟执行环境，然后组合成为完整的Maude模型。（3） 设计并实现了一个OWL-S模型向Maude转换的自动化工具软件。为了提高OWL-S模型转换尤其是批量转换的速度，降低转换过程中引入错误的可能性。在总结了从OWL-S描述的具体模型转换为Maude程序的方法与规则的基础上，设计并开发了一个OWL-S描述的具体模型向Maude程序自动转换的工具。然后对转换得到的Maude程序进行了分析验证。