传统的Web服务技术缺乏机器可理解的语义，限制了Web服务的自动化，语义Web研究的兴起为Web服务技术带来了新的活力，这两种技术的结合产生了另一个新兴的研究课题一语义Web服务，语义Web服务是指用语义Web标记语言来描述服务的语义，使Web服务成为计算机可以理解的实体，实现Web服务操作的智能化和自动化。而语义Web服务组合是语义Web服务的重要目标和研究热点之一，因为单个服务往往无法满足实际的应用需求，需要自动地、动态地组合多个语义Web服务以满足用户的特定需求。 状态演算(Situaltion Calculus)是一种一阶逻辑语言，主要用来表示动态变化的世界，是一种关于状态、动作和动作作用于状态的结果的形式化谓词演算，通过寻找一组动作获得由合式公式描述的目标状态，从而为服务组合提供形式化的规划手段。Pi演算(Pi Calculus)是一种进程代数，允许进程之间传送和接收通道名，能够方便的刻画系统结构的动态变化，且具有很强的表达能力，是一种对系统进行建模和验证的有效形式化方法。 本文首先讨论了Web本体语言描述服务框架(OWL-S)对语义Web服务组合的支持和不足之处，然后对状态演算进行了扩展，在状态演算中增加了意愿公理的表示和描述、引入了次序构词，使其可以处理用户的不同需求和偏好；基于上述扩展使用状态演算对语义Web服务及其组合进行形式化描述，给出一组从OWL-S到状态演算的映射，在时通过形式化的推理来得出服务的组合系列。 在对语义Web服务及其组合进行形式化描述的基础上，借助Pi演算的操作语义和自动推演能力将验证过程转化成并行进程的推演过程，实现对服务组合中服务间行为兼容性的验证，从而保证语义Web服务组合的正确性和完整性。 基于本文的语义Web服务组合及验证工作，设计了一个语义Web服务组合框架，基于该框架对语义Web服务组合实例进行了分析，表明了状态演算和Pi演算是对语义Web服务及其组合进行形式化描述和验证的有效手段。