随着Web服务数量的急剧增多,用户面临大量的服务选择。因此如何从众多功能相似的Web服务中高效地发现满足条件的服务,如何判定服务组合的正确性等问题,已成为业界研究的热点。其中,恰当的描述Web服务及其组合,刻画其相似性、组合正确性等性质是当前首要解决的问题。历史上先后出现了大量Web服务的描述语言,然而它们大多都是非形式化的。为了更精确的描述和讨论服务及其组合的性质,本文引入形式化方法构建了Web服务的一个理论模型,并以此为基础讨论了Web服务的等价性。具体来说,研究内容主要包括以下几个方面。首先,本文在传值CCS系统的基础上,提出了SVCCS系统。该系统不仅可以描述进程的交互行为,还能够刻画其结构特点。在此基础上,进一步引入了互模拟的概念来讨论进程的等价性问题。考虑到进程描述的简洁性要求及其等价验证的计算复杂性要求,本文采用符号化思想将SVCCS系统进一步改进为S-系统,同时证明了两者所刻画的进程等价关系是一致的。其次,本文引入了一个Web服务的形式化模型,SMWS。该模型的理论基础是S-系统。一方面,SMWS模型提供了描述Web服务基本特征:输入、输出、前提和效果的必要手段。另一方面,它使用互模拟的思想,给出了一个Web服务等价性判定的具体方法。最后,以SMWS模型为基础,本文提出了一个具体的Web服务的调用框架。它通过引入基于SMWS模型的进程的匹配算法,来验证Web服务的相似性,并以此算法为支撑来验证服务组合的正确性。