Web服务技术通过使用一系列的标准规范,为互联网上的不同应用提供了语法互操作性支持,使得企业之间的应用交互从局部范围发展到全球范围成为可能。利用Web服务技术进行交互的应用只需遵从相应的Web服务接口,而不需考虑各自的内部实现,从而极大地降低了交互应用之间的耦合度,增加了企业应用的灵活性。因此,Web服务技术已经逐渐成为实现企业内应用集成和企业间应用交互的主流技术。由于Web服务的松散耦合特性,其在提高应用灵活性的同时,也引出了新的研究问题,即如何保证两个独立开发的应用之间的Web服务接口能够互操作。当前的Web服务技术只能在语法上为不同应用的Web服务接口提供互操作性支持,而Web服务接口的语义互操作性问题尚有待解决。本文使用形式化的方法对Web服务接口的相容性和调解问题进行了研究,给出了它们的严格定义并设计了一系列相关的算法,具体内容包括:1)研究了Web服务接口应含信息的界定问题。通过分析Web服务的交互行为,指出了一个Web服务接口应当包含两个部分:消息描述和流程描述。其中,消息描述定义一个Web服务接口所支持的所有消息的模式和方向,流程描述定义一个Web服务接口与其伙伴的所有消息交换之间的依赖关系。2)研究了Web服务接口中消息之间的相容性问题。给出了一种基于领域本体的Web服务消息注解方法,并对带注解的Web服务消息进行了形式建模。基于消息的形式模型,定义了Web服务接口的消息相容性,并给出了相应的判定算法。为了对不完全相容的Web服务消息进行处理,还提出了一种消息相容程度的量化方法,对Web服务接口的消息相容度进行了定义,同时也给出了相应的计算算法。3)研究了Web服务接口中流程之间的相容性问题。为Web服务流程提出了一个形式模型并给出了从流程描述到流程模型的转换方法。基于流程的形式模型,研究了两个流程的交互中可能发生的三种异常性质:未指定接收、死锁和活锁。根据这三种异常性质,定义了两个Web服务流程之间的相容性,同时给出了相应的判定算法。为了对不完全相容的Web服务流程进行处理,通过对上述三种异常性质的量化,提出了一种计算两个Web服务流程之间相容度的方法,并给出了相应的计算算法。4)研究了不相容Web服务接口的调解方法。针对不相容的Web服务消息,定义了对消息的相应部分进行转换的属性调解规则和元素调解规则,同时分别给出了不相容消息的属性调解规则和元素调解规则的生成算法。针对不相容的Web服务流程,首先对Web服务的流程模型进行了扩充,给出了适合调解流程的形式模型,并基于该形式模型提出了一个调解流程的生成算法;然后定义了调解流程的相容性和可靠性,并从理论上分别证明了算法所生成的调解流程具有相容性和可靠性。