在语义Web服务的相关研究工作中,以Web服务的组合、发现为目的,已经有大量的研究人员和研究机构对其进行了广泛的研究,其中包括:OWL-S;以工作流为基础的Web服务组合;扩展现有的逻辑并且利用人工智能中的方法建模Web服务.OWLS利用OWL为Web服务构建了一个上层本体来形式化Web服务的主要特征.尽管OWL-S为Web服务建立本体的描述,但是它本身并没有明确对Web服务动态特性的推理,另外,OWL是建立在描述逻辑的基础之上的,描述逻辑可以有效的表示关于静态领域的知识,但是对于具有动态特性的知识如服务和动作却缺乏相应的表示机制.另一方面,虽然OWL-S为了表示动态的特性,引入了描述服务的前提条件和结果等属性,但这些属性却是作为OWL所构建本体的普通的属性来处理,从而缺乏相关的动态的语义支持;而基于工作流的方法虽然可以建模服务流程,形成组合方案,但却缺乏严格的语义定义.　　 类型和类型系统在计算机科学尤其是程序设计语言中被广泛的研究和应用,类型系统可以用以确保系统按照隐式或者显示的说明方式运行,并自动检测程序由于类型错误而引起的语义错误,从而避免不规范的行为的产生.用类型去标注程序,从而可以验证程序在类型层次上的正确性.同样地,用面向对象中的对象去标记程序中的符号,可以验证程序在对象层次上的正确性;用本体中的概念去标注程序中的符号,从而在本体的层面验证程序的正确性.如同在各个层面标注程序中的符号,可以用类型系统中的类型,面向对象中的对象,本体中的概念描述服务中的属性和关系的取值,用以标注整个服务框架.　　 如服务组合是服务中的一个研究问题一样,若两个服务能够组合,则在标注两个被组合服务的属性和关系的类型、对象、本体概念之间应该有某种联系,如何形式地陈述这种关系是本文的主要目的.本文的主要工作可以总结如下三个方面:　　 ·在一阶逻辑和类型论的基础之上,给出了面向Web服务的带类型的一阶逻辑(ζ)T,并且定义了它的语法,讨论了它的对象构造规则和一阶逻辑公式的生成规则,并论证了相应的类型系统中类型的唯一性;研究了(ζ)T的语义,给出了其二元组语义模型(ｍ)T=(UT,τ)的具体定义.在(ζ)T中加入了动作成分,构成了可以形式化Web服务的带类型的一阶动态逻辑(ζ)T21,并且详细给出了语言中动作的类型规则以及带类型的语义模型(ζ)T21,论证了加入了动态成分以后相应的类型唯一性.　　 ·形式地陈述了标注两个被组合服务的属性和关系的类型、对象、本体概念之间的联系,以带类型的一阶动态逻辑为描述语言,给出了描述语义Web服务的带类型的框架OWL-S21,从而使得每个语义Web服务都带有类型,并定义了相应的语法规则和模型的可满足性。　　 ·利用OWL-S21中的约束条件对服务组合的验证中的性质进行了讨论:并且利用类型和子类型的关系,为带类型的框架OWL-S21建立层次结构,从而将该框架组织起来,为形式化Web服务提供有效的支持。