随着Web服务标准的完善和支持Web服务平台的逐步成熟,网络上的可用的服务越来越多,基于Web服务的应用也越来越多。由于当前Web服务所使用的协议都是基于描述基础,缺乏有效的理论或者工具对Web服务的属性进行验证,随着Web服务的深入研究和应用,先天的缺陷严重限制了Web服务的更广泛研究,例如在Web服务自动组合研究领域。 Martin-Lof类型理论是一种适合程序构造的形式系统,可以在同一个形式系统中同时表示规格说明和程序,而且证明规则能够从规格说明导出一个正确的程序以及能检验一个给定程序具有某个性质。利用该理论来描述Web服务的基本元素,同时定义出Web服务相关操作的计算公式以及计算方法,从理论的角度和程序与规则的关系来观察Web服务,尤其是在Web服务的自动组合方面,具有很高的研究价值。 文章的工作主要集中在以下几个方面: 第一,用Martin-Lof类型理论描述Web服务的基本元素。解决了基于描述的各种Web服务相关协议和应用缺乏有力的理论基础的问题。 第二,用Martin-Lof类型理论验证服务匹配问题。文章给出Web服务匹配的计算规则以及Web服务分类的计算公式及其计算方法,并且根据问题说明得出服务匹配验证结果。 第三,作为一个理论基础,类型理论可以从推导过程给出Web服务相关应用的计算方法,描述一个基于Martin-Lof类型理论的服务匹配平台,着重描述在具体应用平台上实现Web服务的匹配工作,为服务自动组合提供理论基础和实践平台。 本工作得到中间件软件平台产品的研制及产业化(浙江省重点科研项目,2004C11053)的资助。