在网络飞速发展的今天，Web服务已成为一种非常重要的技术．Web服务的形式化表示是面向服务的计算的基础，形式化Web服务不仅可以更好地理解Web服务的本质，而且可以更深入地分析Web服务的各种性质．　　 Web服务有几种形式化表示：WSMO(Web服务建模本体)和OWL-S(Web服务本体语言)．WSMO是描述语义Web服务的一个概念模型，为语义Web服务建立统一的体系结构和共同的平台．OWL-S是用OWL语言描述Web服务的本体，主要描述Web服务的属性和功能，解决Web服务描述和发现以及业务组合的语义表示的问题.　　 本文提出了一个可以描述Web服务的一阶动态逻辑，并用该逻辑对Web服务进行形式化．Web服务的能力是通过前置状态和后置状态的改变体现的，而一阶动态逻辑利用模态算子将动作与状态的变化联系起来，并且通过状态的变化描述某个动作．一阶动态逻辑是形式化程序和程序动态行为的逻辑，它形式化存储中变量值的改变，在其语义中，可能世界就是对变量的赋值.但是，在Web服务中，不仅包含程序，还包含其他的服务，而有些服务会改变应用这些服务时涉及到的对象具有的属性和关系，因此，用传统的一阶动态逻辑描述Web服务己不再恰当．本文在一阶动态逻辑的基础上对其语法和语义进行扩展与改进，扩展后的一阶动态逻辑不仅可以描述改变变量的程序动作的动态性质，还可以描述改变关系的服务动作的动态性质.本文通过用扩展后的一阶动态逻辑对一个购书Web服务实例进行形式化，展示了本文提出的Web服务描述方法的可行性，以及该方法相比于其它Web服务形式化描述方法的特色.