近年来,Web服务研究领域的一个重要研究方向是探讨如何组合已有的Web服务并协调其运行以便于更有效地利用网络上已有的服务。为此,人们提出了很多Web服务编排语言。在已经出现的若干编排语言中WS-BPEL最有可能成为该领域的标准。WS-BPEL利用长期运行事务和补偿这两个概念对错误进行了处理。为了形式化地刻画WS-BPEL,Manuel Mazzara和Ivan Lanese提出了一种新的进程演算系统Webπ∞。Manuel Mazzara和Ivan Lanese给出了Webπ∞的归约语义和LTS语义,并在此基础上分别定义了弱B-同余(Weak Barbed Congruence)和封闭互模拟(Closed bisimilarity),并证明了封闭互模拟相对弱B-同余的可靠性。但由于α?不是图像有限的,目前还未得到一个完备性的结果。本文主要探讨在强情形下Webπ∞的行为理论,研究内容包括:(1)讨论了强情形下相关概念及基本性质,包括进程上的强B-同余关系,强封闭互模拟c～a。(2)引入了一个安全函数,基于该函数定义了Up-To上下文的强封闭互模拟关系,进而给出了强封闭互模拟～ca的一个Up-To证明技术。(3)利用上述的Up-To证明技术,证明了强封闭互模拟相对于强B-同余的可靠性。(4)证明了?α?→的图像有限性,在此基础上完成了强封闭互模拟～ca相对于强B-同余的完备性定理的证明。