（计算机应用技术专业论文）类型理论在web服务描述和验证方面的应用.pdf

浙江大学硕士学位论文 摘要 随着w e b 服务标准的完善和支持w e b 服务平台的逐步成熟，网络上的可用的 服务越来越多，基于w e b 服务的应用也越来越多。由于当前w e b 服务所使用的协 议都是基于描述基础，缺乏有效的理论或者工具对w e b 服务的属性进行验证，随 着w e b 服务的深入研究和应用，先天的缺陷严重限制了w e b 服务的更广泛研究， 例如在w e b 服务自动组合研究领域。 m a r t i n l o f 类型理论是一种适合程序构造的形式系统，可以在同一个形式 系统中同时表示规格说明和程序，而且证明规则能够从规格说明导出一个正确的 程序以及能检验一个给定程序具有某个性质。利用该理论来描述w e b 服务的基本 元素，同时定义出w e b 服务相关操作的计算公式以及计算方法，从理论的角度和 程序与规则的关系来观察w e b 服务，尤其是在w e b 服务的自动组合方面，具有很 高的研究价值。 文章的工作主要集中在以下几个方面： 第一，用m a r t i n l o f 类型理论描述w e b 服务的基本元素。解决了基于描述 的各种w e b 服务相关协议和应用缺乏有力的理论基础的问题。 第二，用m a r t i n l o f 类型理论验证服务匹配问题。文章给出w e b 服务匹配 的计算规则阻及w e b 服务分类的计算公式及其计算方法，并且根据问题说明得出 服务匹配验证结果。 第三，作为一个理论基础，类型理论可以从推导过程给出w e b 服务相关应用 的计算方法，描述一个基于m a r t i n l o f 类型理论的服务匹配平台，着重描述在 具体应用平台上实现w e b 服务的匹配工作，为服务自动组合提供理论基础和实践 平台。 本工作得到中间件软件平台产品的研制及产业化( 浙江省重点科研项目， 2 0 0 4 c 1 1 0 5 3 ) 的资助。 关键词：w e b 服务，类型理论，匹配，服务组合。 浙江大学硕士学位论文 a b s t r a c t w i t ht h ed e v e l o p m e n to ft h es p e c i f i c a t i o n sa n dp l a t f o r m sf o rw e bs e r v i c e ，m o r e a n dm o r ew e bs e r v i c e sc a nb ea c c e s s e de a s i l ya sw e l la st h ea p p l i c a t i o n sb a s e do n w e bs e r v i c e h o w e v e rt h ec u r r e n tp r o t o c o lf o rw e bs e r v i c e sa r ea l m o s td e s c r i b a b l e w i t h o u tt h es u p p o r tf r o mt h eb a s i ct h e o r ya n dt h et o o l sf o rt h ev e r i f i c a t i o n w 曲t h e d e e pr e s e a r c ha b o u tw 曲s e r v i c e s d i s a d v a n t a g el i m i t st h ed e v e l o p m e n to fw e b s e r v i c e ，f o re x a m p l e ，t h ea r e ao f a u t o m a t ec o m p o s i t i o no f w e bs e r v i c e s i nr e c e n t y e a r ss e v e r a l f o r m a l i s m sf o rp r o g r a mc o n s t r u c t i o nh a v e b e e n i n t r o d u c e d o n es u c hf o r m a l i s mi st h et y p et h e o r yd e v e l o p e db yp e rm a r t i n l o f i ti s w e l ls u i t e da sat h e o r yf o rp r o g r a mc o n s t r u c t i o ns i n c ei ti sp o s s i b l et oe x p r e s sb o t h s p e c i f i c a t i o n sa n dp r o g r a m sw i t h i nt h es a m ef o r m a l i s m f u r t h e r m o r e ，t h ep r o o fr u l e s c a nb eu s e dt od e r i v eac o r r e c tp r o g r a mf r o mas p e c i f i c a t i o na sw e l la st ov e r i f yt h a ta g i v e np r o g r a mh a sac e r t a i np r o p e r t y t h e ni ti sas u i t a b l et h e o r yf o rt h er e s e a r c ho f w e bs e r v i c e s ，e s p e c i a l l y f o r t h e a r e a o f a u t o m a t ec o m p o s i t i o n o f w e bs e r v i c e s i nt h ep a p e r , o u rc o n t r i b u t i o n sf o rt h ew e bs e r v i c e sa r ed e s c r i b e db e l o w ： f i r s t l y , w ew i l ld e f i n ea l lt h eb a s i ce l e m e n t si nw e bs e r v i c eu s i n gm a r t i n - l o f s t y p et h e o r y i nt h em e a n w h i l e ，w ew i l ls h o wt h ed e f m i t i o no ft h em a t c h i n go fw e b s e r v i c e sa n dt h ec a l c u l a t i o no f t h em a t c h i n g s e c o n d l y ，w e w i l ld e s c r i b et h ev e r i f i c a t i o no fm a t c h i n gf o rw e bs e r v i c e a c c o r d i n gt ot h ed e f i n i t i o n ，w ew i l lg i v et h ep r o c e s so f c o m p u t ef r o mt h ed e s c f i p t i o n l a s t l y , w ew i l lg i v et h ed e t a i l sa b o u tap l a t f o r mw h i c hw i l li m p l e m e n tt h e m a t c h i n ga n dv e i l l y i n gf o rw e bs e r v i c e su s i n gm a r t i n - l o ft y p et h e o r y i ti st h eb a s i c p r o j e c tf o rt h ea u t o m a t e dc o m p o s i t i o nf o rw e bs e r v i c e s k e yw o r d s ：w e bs e r v i c e ，t y p et h e o r y ，m a t c h i n g ，c o m p o s i t i o n 。 4 浙江大学硕士学位论文 1 1 引言 第一章绪论 w e b 服务的出现，提高了互联网资源的重用性，随着w e b 服务标准“2 “”的提 出，w e b 服务已经越来越多的使用到企业的应用中去，当前w e b 服务提供了很多 的通讯协议，保证分布于世界各地的用户顺利注册、查询、调用等服务操作，例 如w s d l “3 、u d d i 。3 、s o a p 。3 等等。然而这些服务基本上都是基于描述层次，缺乏 有效的机制或者工具来验证w e b 服务的相关属性。类型理论是计算机的基础数 学，具有强大的程序推导和程序验证功能，用其来描述和验证w e b 服务，为w e b 服务的深层次应用提供了坚实的基础。 随着计算机科学基础的发展，在高层的应用往往基于这些基础，反之，在高 层应用所获得成就和理论可以反过来促进计算机科学基础的反展与研究。由简如 繁，由繁化间，周而复始，形成了计算机科学发展的规律。 文章将计算机科学基础理论m a r t i n l o f 类型理论嘲“”的基础上来思考 高层应用w e b 服务的应用，从程序语言的设计角度最基本的类型来观 察w e b 服务各个应用。即可以用m a r t i n l o f 类型理论来描述w e b 服务的最基本 单元，用这些基本单元来描述w e b 服务的应用，如w e b 服务自动组合、w e b 服务 自动查找、w e b 服务验证、w e b 服务匹配等方面。从计算机的基础角度来观察高 层应用，反过来促进高层应用的发展和进步。 1 2w e b 服务简介 w e b 服务在w 3 c 中有很多的定义： 定义一：w e bs e r v i c e s 是自包含的、模块化的应用程序，它可以在网络( 通 常为w e b ) 中被描述、发布、查找以及调用。 定义二：w e bs e r v i c e s 是基于网络的、分布式的模块化组件，它执行特定 的任务，遵守具体的技术规范，这些规范使得w e bs e r v i c e 能与其他兼容的组件 进行互操作。 定义三：所谓w e b 服务，它是指由企业发布的完成其特别商务需求的在线应 用服务，其他公司或应用软件能够通过i n t e r n e t 来访问并使用这项应用服务。 ( u d d i 规范2 0 ) 总而言之，w e b 服务是能够支持不同机器问的应用通过互联网实现交互的软 件系统，它的接口使用机器能够解析的格式( 一般来说是w s d l 格式) 进行描述， 其他系统按照人为约定的方式使用s o a p 消息访问w e b 服务的接口5 佰2 3 ) 1 5 1 。w e b 浙江大学硕士学位论文 服务发布后，使用u d d i 来进行服务查找和定位。 w e b 服务体系结构是面向对象分析与设计( o o a d ) 的一种合理发展 ( 1 0 9 i c a le v o l u t i o n ) ，同时也是电子商务解决方案中，面向体系结构、设计、 实现与部署而采用的组件化的合理发展。w e b 服务基于分布式计算，一个完整的 w e b 服务架构包括三种角色( 或者运行时环境) ： 圈1 1w e b 月畏务三个角色之间的关系 服务提供者：包括以下两种角色： 服务接口提供者：提供访问应用的接口作为w e b 服务 服务提供者；提供可执行的应用程序作为w e b 服务。 服务注册中心：作为w e b 服务的代理，服务提供者在此发布他们的服务 描述。 服务请求者：是请求使用w e b 服务的应用程序( 客户端) 。最终用户可 以通过一个p o r t a l 或蜂窝电话来访闯w e b 服务。 通过w e b 服务的定义可以看出，w e b 服务主要包括以下3 项技术： - s o a p ( s i m p l eo b j e c ta c c e s sp r o t o c 0 1 ) 是w e bs e r v i c e 最关键的技术。 它是w e bs e r v i c e 中数据和方法调用传输的介质。 s o a p 是一个基于x m l 的协议，它包括三个部分：s o a p 封装( e n v e l o p ) ，封装 定义了一个描述消息中的内容是什么，是谁发送的，谁应当接受并处理它以及如 何处理它们的框架；s o a p 编码规则( e n c o d i n gr u l e s ) ，用于表示应用程序需要 使用的数据类型的实例：s o a pr p c 表示( r p cr e p r e s e n t a t i o n ) ，表示远程过程 调用和应答的协定：s o a p 可以和多种传输协议绑定( b i n d i n g ) ，使用底层协议交 换信息。 w s d l ( w e bs e r v i c ed e f i n i t i o nl a n g u a g e ) 描述了w e bs e r v i c e 的接口和 功能。 w s d l 用x m l 格式将网络服务定义为一组端点，这组端点是对包含面向文档 或面向过程信息的消息进行操作的。这些操作和消息的描述是抽象的，然后将它 们绑定到具体的网络协议和消息格式以定义端点。相关的具体端点都组合为抽象 的端点服务。w s d l 可扩展来允许描述端点及其消息，而不必考虑使用什么样的 6 浙江大学硕士学位论文 消息格式或网络协议来进行通信。这意味着使用x m l 模式来简要地定义接口而后 将这些接口绑定到适用于该协议的具体表示法。 u d d i ( u n i v e r s a ld e s c r i p t i o n ，d i s c o v e r ya n di n t e g r a t i o n ) 就像一个 电话目录，记载了所有可用的w e bs e r v i c e s 。 统一描述、发现和集成规范( u d d i ) 创建了一个平台独立，开放的框架，通 过i n t e r n e t 来描述服务，发现商务，并且整合商业服务。它是一套基于w e b 的、 分布式的、为w e b 服务提供的信息注册中心的实现标准规范，同时也包含一组使 企业能将自身提供的w e b 服务注册以使得别的企业能够发现的访问协议的实现 标准。 1 3m a r t in - l o f 类型理论 现代软件工程应用广泛的形式方法来确保系统按照那些对其应有的行为进 行隐式或显式的说明方式来实现。一方面是强有力的框架理论，像h o a r e 逻辑、 代数说明语言、模态逻辑和指称语义；这些框架虽然能表述十分普遍且正确的性 质，但难以使用，且对程序员也提出了更高的要求。另一方面是能力适度的技术 适度到能够将自动检查器放到编译器、连接器或程序分析器中，这样能够被 不熟悉所基于的理论的程序员所使用。这种轻量级形式方法的一个典型实例就是 模型检查器，作为芯片设计或者通讯协议这样的有限状态系统中搜索错误的工 具。另一个越来越引起重视的实例就是实时检测，使一个系统能动态地监测到它 的部件是否处在说明所要求的状态中的技术。但至今最流行的和发展最完善的轻 量级的形式方法就是类型系统。 所谓类型系统是指一种根据所计算出值的种类对词语进行分类从而证明某 程序行为不会发生的可行语法手段。 这个定义确定类型系统作为程序的推导工具。这句话反映了对待程序语言中 类型系统的态度。更一般地，类型系统( 或类型理论) 是指在逻辑、数学和哲学 中更广泛的一类研究领域。m a r t i n l o f 类型理论就是1 9 7 3 年由m a r t i n l o f 针 对这些研究热点，提出的基于构造数学的理论。 m a r t i n l o f 类型理论起源于构造数学”1 ，但区别于绝大多数其他的数学形式 化，类型论不是基于一阶谓词演算。反过来，谓词逻辑通过命题和集合之间的对 应被解释于类型理论中。一个命题就是一个集合，其元素代表该命题的证明。因 此一个假命题被认为空集合以及一个真命题为非空集合。 m a r t i n l o f 类型理论是一种程序构造的形式系统，因此它很合适作为程序 构造的理论，因为在同一个形式系统中能够同时表示规格说明和程序。而且，证 明规则能够从规格说明到处一个正确的程序以及能检验一个给定程序具有某个 性质。作为程序设计语言，m a r t i n l o f 类型理论类似于带类型的函数式语言如 浙江大学硕士学位论文 m o p 。1 和m 【。“”2 “，但是区别在于一个良好类型程序的求值总是能够终止的。 在m a r t i n l o f 类型中，写出程序设计的目的规则说明以及发展大概正确的程序 是可能的。因此类型理论比程序设计语言更加广泛。 1 4自动f f e b 服务 随着w e b 服务的深入应用，通过利用w e b 上人和机器都能够存取的内容，创 建智能自动服务及商务处理基础设施，成为了w e b 服务建设和发展的首要目标。 自动w e b 服务发现：自动w e b 服务发现包括w e b 服务的自动定位。 自动w e b 服务调用：目前许多的w e b 服务在执行过程中需要人的频繁干预 例如在某个w e b 站点购书，用户需要填写购书的表单并提交。有时为了完成一次 w e b 服务的执行，需要用户和w e b 服务之间多次交互。 自动w e b 服务合成和互操作：这个任务包括了w e b 服务的自动选择、合成和 互操作来完成一个任务。复杂的w e b 服务一般由许多小的w e b 服务组合而成例 如：安排一次会议就可能包括了预定机票，预定客房等各种由不同服务提供者提 供的服务。 自动w e b 服务执行监控：在一个复杂的服务执行期间，用户经常需要跟踪和 查询服务及其组件执行过程中状态的变化。 在这个方面，国内外往往在w e b 服务的基础上引入语义的概念，构造语义 w e b 服务，目前在w e b 服务研究方面主要着眼于两个方面：一方面是创建一种计 算机之间能够互相理解的并能充分表示w e b 服务的内容、功能、属性、接口以 及规则和限制条件的语言；另一方面是在这种语言基础之上提出一种使w e b 服 务之间能够实现自动发现、选取、执行、合成以及交互的模型或体系结构。 现有的w e b 服务的工业标准( 诸如s o a p 、w s d l 、u d d i 等) 能否用来描述智 能w e b 服务呢? 实际上这些工业标准主要能够实现w e b 服务的自动发现和调用， 但是由于这些工业标准缺乏理论基础和有效的验证工具，限制了其深入应用。 1 5服务组合相关项目和平台 目前，尚无基于m a r t i n l o f 类型理论或者任何类型系统的服务平台，因此 这里仅列出单纯服务组合的相关项目和平台。 服务组合问题的研究已经吸引了学术界和工业界的广泛关注，与此相关的平 台研制和产品开发也大量开展起来。目前大多数的服务组合平台和产品，如都是 基于工作流管理系统的框架，并在此基础上增加服务相关的功能组件。综合现有 的一些平台和产品，我们得出如图卜2 所示的基于工作流的服务组合平台通用框 架。 在通用服务组合平台的体系结构之上，不同的平台和产品都会有所扩充。下 浙江大学硕士学位论文 h o p 和m l 1 。1 ”2 。! ，但是区别在于一个良好类型程序的求值总是能够终l r 的。 在m a r t i n l o f 类型巾，写出程序设计的目的规则说明以及发展大概正确的程序 是可能的。因此类型理论比程序设训语言更加广泛。 1 4自动w e b 服务 随着w e b 服务的深入应用，通过利用w e b 上人和机器都能够存取的内容，创 建智能自动服务及商务处理基础设施，成为了w e b 服务建设和发展的首要日标。 自动w e b 服务发现：自动w e b 服务发现包括w e b 服务的自动定位。 自动w e b 服务调用：目前许多的w e b 服务在执行过程中需要人的频繁干预 例如在某个w e b 站点购书，用户需要填写购书的表单并提交。有时为了完成一次 w e b 服务的执行，需要用户和w e b 服务之间多次交互。 自动w e b 服务合成和互操作：这个任务包括了w e b 服务的自动选择、合成和 互操作来完成一个任务。复杂的w e b 服务一般由许多小的w e b 服务组合而成例 如：安排一次会议就可能包括了预定机票，预定客房等各种由不同服务提供者提 供的服务。 自动w e b 服务执行监控；在一个复杂的服务执行期间，用户经常需要跟踪和 查询服务及其组件执行过程中状态的变化。 在这个方面，国内外往往在w e b 服务的基础上引入语义的概念，构造语义 w e b 服务，目前在w e b 月k 务研究方面主要着眼十两个方面：一方面是创建一种计 算机之间能够互相理解的并能充分表示w e b 服务的内容、功能、属性、接u 以 及规则和限制条件的语言；另一方面是在这种语言基础之上提出一种使w e b 服 务之问能够实现自动发现、选取、执行、合成以及交互的模型或体系结构。 现有的w e b 服务的工业标准( i l l 如s o a p 、w s i ) l 、u d d i 等) 能否用来描述智 能w e b 服务呢? 实际上这些丁业标准主要能够实现w e b 服务的自动发现和调用， 但是由于这些工业标准缺乏理论基础和有效的验证工具，限制了其深入应用。 i 5 服务组合相关项目和平台 目前，尚无基于m a r t i n l o f 类型理论或者任何类型系统的服务平台，因此 这里仅列出单纯服务组合的相关项目和平台。 服务组合问题的研究已经吸引了学术界和工业界的广泛关注，与此相关的平 台研制和产品开发也大量开展起来。目前大多数的服务组合平台和产品，如都是 基丁工作流管理系统的框架，并在此基础上增加服务相关的功能组件。综合现有 的一些平台和产品，我们得出如图卜2 所示的基于工作流的服务组合平台通用框 架。 在通用服务组合平台的体系结构之上不同的平台和产品都会有所扩充。下 在通用服务组合平台的体系结构之上，不i 刊的、r 台和产品都会有所扩充。下 浙江大学硕士学位论文 m o p 。1 和m 【。“”2 “，但是区别在于一个良好类型程序的求值总是能够终止的。 在m a r t i n l o f 类型中，写出程序设计的目的规则说明以及发展大概正确的程序 是可能的。因此类型理论比程序设计语言更加广泛。 1 4自动f f e b 服务 随着w e b 服务的深入应用，通过利用w e b 上人和机器都能够存取的内容，创 建智能自动服务及商务处理基础设施，成为了w e b 服务建设和发展的首要目标。 自动w e b 服务发现：自动w e b 服务发现包括w e b 服务的自动定位。 自动w e b 服务调用：目前许多的w e b 服务在执行过程中需要人的频繁干预 例如在某个w e b 站点购书，用户需要填写购书的表单并提交。有时为了完成一次 w e b 服务的执行，需要用户和w e b 服务之间多次交互。 自动w e b 服务合成和互操作：这个任务包括了w e b 服务的自动选择、合成和 互操作来完成一个任务。复杂的w e b 服务一般由许多小的w e b 服务组合而成例 如：安排一次会议就可能包括了预定机票，预定客房等各种由不同服务提供者提 供的服务。 自动w e b 服务执行监控：在一个复杂的服务执行期间，用户经常需要跟踪和 查询服务及其组件执行过程中状态的变化。 在这个方面，国内外往往在w e b 服务的基础上引入语义的概念，构造语义 w e b 服务，目前在w e b 服务研究方面主要着眼于两个方面：一方面是创建一种计 算机之间能够互相理解的并能充分表示w e b 服务的内容、功能、属性、接口以 及规则和限制条件的语言；另一方面是在这种语言基础之上提出一种使w e b 服 务之间能够实现自动发现、选取、执行、合成以及交互的模型或体系结构。 现有的w e b 服务的工业标准( 诸如s o a p 、w s d l 、u d d i 等) 能否用来描述智 能w e b 服务呢? 实际上这些工业标准主要能够实现w e b 服务的自动发现和调用， 但是由于这些工业标准缺乏理论基础和有效的验证工具，限制了其深入应用。 1 5服务组合相关项目和平台 目前，尚无基于m a r t i n l o f 类型理论或者任何类型系统的服务平台，因此 这里仅列出单纯服务组合的相关项目和平台。 服务组合问题的研究已经吸引了学术界和工业界的广泛关注，与此相关的平 台研制和产品开发也大量开展起来。目前大多数的服务组合平台和产品，如都是 基于工作流管理系统的框架，并在此基础上增加服务相关的功能组件。综合现有 的一些平台和产品，我们得出如图卜2 所示的基于工作流的服务组合平台通用框 架。 在通用服务组合平台的体系结构之上，不同的平台和产品都会有所扩充。下 浙江大学硕士学位论文 面我们将对国内外几个主要的服务组合项目和平台进行介绍，包括国外的e f l o w 平台、m e t e o r s 项目和s e l f s e r v 项目以及国内的f l a m e 2 0 0 8 平台。 搬 图1 2 基于工作流的服务组合平台通用框架 1 4 te f l o w 平台 e f l o w 【1 4 】【”】是h p 公司较早推出的一个基于工作流方法的支持服务组合设计、 部署、运行和脏控的服务平台。该平台是在服务基础平台e s p e a k 之上，结合工 作流方法进行开发的。e f l o w 支持将各种应用( 特别是j a v a 对象) 部署为w e b 服务，支持服务的注册、查询和调用。通过扩展工作流的基本概念和模型，e f l o w 提出了服务组合模型s c m ( s e r v i c ec o m p o s i t i o nm o d e l ) ，该模型将一个服务组 合表示为一个流程模式( p r o c e s ss c h e m a ) ，包含服务节点、判断节点和事务节 点等关键元素，支持服务组合的嵌套定义。基于s c m 提出了服务组合定义语言 c s d l ( c o m p o s i t es e r v i c ed e s c r i p t i o nl a n g u a g e ) ，支持服务组合的静态组合 和服务的动态绑定。e f l o w 的特点在于采用了柔性工作流的“黑盒”方法( 即将 流程的不确定的子流和结构用“黑盒”封装，而在服务组合执行中根据实例信息 将“黑盒”具体化而形成完整定义) ，提高服务组合的流程柔性和对业务变化的 应对能力。此外，e f l o w 还具有可配置( c o n f i g u r a b l e ) 的特点，用户可根据不 同的目标应用对e f l o w 的功能模块进行裁减，得到最合适的系统配置。然而e f l o w 只支持运行前的服务绑定，动态性和灵活性不够，此外服务( 服务组合) 的注册 和查询缺乏语义支持，准确率和效率有待改善。 1 4 2 m e t e o r s 项目 m e t e o r s 16 l 项目是由美国乔治亚大学的l s d i s 实验室承担的服务综合管理 项目。该项目旨在结合工作流、语义网、w e b 服务三种技术以解决语义w e b 服务 的描述、发现、组合和执行问题。m e t e o r s 包含两大功能模块：服务发现基础 构架m w s d i ( m e t e o r sw e bs e r v i c ed is c o v e r yi n f r a s t r u c t u r e ) 和服务组合 框架m w s c f ( m e t e o r sw e bs e r v i c ec o m p o s i t i o nf r a m e w o r k ) 。为了解决服务 查询的准确高效问题，m w s d i 一方面增强了标准w e b 服务在接口、参数、功能和 9 浙江大学硕士学位论文 q o s 等描述的语义支持，另一方面采取了分布式的p 2 p 语义存储和注册机制。 m w s c f 提出了语义w e b 流程( s e m a n t i cw e bp r o c e s s ) 的概念( 即服务组合的各 成员服务均通过语义进行描述) ，将服务组合流程分成抽象流程和可执行流程两 个不同层次，前者采用语义服务模板、语义流程模板和抽象服务接口来描述目标 服务以达到动态绑定的目的，后者采用语义本体论推理和q o s 策略相结合的服务 匹配和筛选方法，能准确快速的获取满足业务需求的目标服务。由于m w s c f 目前 只实现了服务组合的设计，而服务组合执行引擎是基于i b m 的b p e l 4 j 执行引擎， 不仅缺乏对服务组合执行的有效控制，而且要求在执行前完成抽象流程到可执行 的b p e l 4 w s 流程的转换，所以m w s c f 和e f l o w 一样动态性不够。 1 4 3 s e l f s e r v 项目 s e l f s e r v t l 是澳大利亚新南威尔士大学和昆士兰大学合作研制的一个快速 开发和执行的服务组合平台。该平台使用离散状态图s t a t e c h a r t 进行服务组合 建模，其中每个状态表示一次原子服务或者组合服务的调用，转移条件使用e c a 规则表示。由于s t a t e c h a r t 具有形式化语义，因此能够准确无误的解释和分析 服务组合流程。s e l f s e r v 将服务按照粒度分为三种：基本服务、组合服务和社 区服务，其中社区服务是一类具有相同功能和接口的服务描述。s e l f s e r v 在服 务组合建模中，可以为状态指定社区服务，而不必指定一个特定的服务，以此来 实现在运行时服务的动态选取和绑定，因此具有很好的动态性和灵活性。不同于 e f l o w 和m e t e r s 平台的集中式执行方式( 即存在一个中央执行引擎，各成员服 务都是通过执行引擎间接进行交互) ，s e l f s e r v 采用p 2 p 的执行方式，实现成 员服务之间的直接交互，从而避免了中央执行引擎在通信和效率上的瓶颈。参与 执行的每一个成员服务都自动从s e l f s e r v 环境中下载一个协调器 ( c o o r d i n a t o r ) 、封装器( w r a p p e r ) 和路由表( r o u t i n gt a b l e ) 以实现p 2 p 的执行，协调器实现服务之间的消息传递和消息处理，封装器将服务封装成 s e l f s e r v 中定义良好的对外接口，路由表则是成员服务在组合中的位置信息。 s e l f s e r v 目前只支持关键字级别的服务查询，与e f l o w 一样缺乏语义支持。此 外在p 2 p 的方式下进行执行监控和异常处理也是s e l f s e r v 目前面临的问题。 1 4 4 f l a m e 2 0 0 8 平台 f l a m e 2 0 0 8 1 8 l 是由中国科学院计算所和德国弗朗霍夫软件研究所合作开发的 面向北京2 0 0 8 年奥运会的一套服务中间件平台，旨在通过整合奥运会期间各种 自治的社会服务，为各类用户提供即时服务组合支撑环境，从而帮助业务用户在 业务层面组合配置各类服务形成应用，以满足用户个性化的应用需求。该平台的 特点在于将服务组合应用的开发分成业务层( b u s i n e s s l e v e l ) 设计和软件层 ( s o f t w a r e l e v e l ) 设计，并且基于这种分层设计思想提出了一种服务组合模型 1 0 浙江大学硕士学位论文 c a f i s e 。在该模型中，最终用户通过业务层的服务组合和配置形成目标业务逻辑。 为准确描述业务逻辑过程和业务需求，c a f i s e 设计了一种服务组合语言v i n c a 。 不同于现有的其它服务组合语言，v i n c a 是面向最终用户的业务配置语言，它从 业务层面描述了用户个性化应用需求，具有所见即所得的特点。v i n c a 语言既支 持服务的静态绑定，也支持运行时的服务绑定，因此f l a m e 2 0 0 8 具有很好的动态 性和对业务环境变化的应对能力。c a f i s e 根据业务层与软件层之间的服务映射 关系、控制逻辑映射关系等，将服务组合的v i n c a 描述自动转换到软件层的 b p e l 4 w s 描述。f l a m e 2 0 0 8 平台将业务服务根据特点领域的语义本体论划分成不 同的服务社区，很好的支持了服务( 组合服务) 在语义层的注册和查询。然而该 平台目前尚在不断完善阶段，目前的实现还缺乏对v i n c a 语言描述业务逻辑时的 正确性验证以及对服务组合执行过中的有效监控和管理。 1 6文章的结构和组织 文章介绍了基于m a r t i n l o f 类型理论的w e b 服务研究，利用该理论对w e b 服务基本元素，给出w e b 服务匹配的程序推导过程，并且提供了一个基于此研究 的服务组合平台_ d a r t f l o w 平台，提供基于m a r t i n - - l o f 类型理论的w e b 服 务匹配和验证功能。本文的组织结构如下： 第一章介绍了w e b 服务和m a r t i n l o f 类型理论在高层应用方面的优势和能 力，并分析现有的服务相关项目和平台，为以后的平台设计提供参考。 第二章介绍了m a r t i n l o f 类型理论，介绍了该理论在程序推导方面的优势。 第三章介绍了m a r t i n l o f 类型理论在w e b 服务描述方面的研究，分析了w e b 服务的基本元素，提供了基本元素在m a r t i n l o f 类型理论中的映射。 第四章介绍了m a r t i n l o f 类型理论在w e b 服务匹配方面的研究，分析了w e b 服务匹配程序的推导过程 第五章介绍d a r t f l o w 平台的基础工作，主要从总体上介绍了d a r t f l o w 平台 的结构，如何实现m a r t i n l o f 类型理论在描述和验证方面的实现，并简要的介 绍了d a r t f l o w 平台各个模块的功能。 最后对整个算法和平台进行总结，并提出了对m a r t i nl o f 类型理论在w e b 服务应用方面的后续深入研究工作。 浙江大学硕士学位论文 2 1引言 第二章m a r t i n l o f 类型理论 m a r t i n l o f 类型理论是一种程序构造的形式系统，它很合适作为程序构造 “”的理论，因为在同一个形式系统中能够同时表示规格说明和程序。而且，证 明规则能够从规格说明到处一个正确的程序以及能检验“”一个给定程序具有某 个性质。作为程序设计语言，m a r t i n l o f 类型理论类似于带类型的函数式语言 如h o p 和m l ，但是区别在于一个良好类型程序的求值总是能够终止的。在 m a r t i n i ，o f 类型中，写出程序设计的目的规则说明以及发展大概正确的程序是 可能的。因此类型理论比程序设计语言更加广泛。 当定义程序设计语言的时候，通常使用数学对象，例如集合、函数等，来解 释程序所描述的对象。大部分的程序设计语言在描述这些数学对象采取定义的方 式来解释其含义。例如，很多程序语言中都存在函数的概念，其通用的定义方式 是提供o 到多个参数，返回0 到多个值。同样m a r t i n l o f 类型理论也必须在其 理论中给出这些数学对象的定义，在m a r t i n l o f 类型理论中，称为t y p e ( 类型) 。 换句话丽言，m a r t i n l o f 类型理论中所使用的数学对象都必须首先得到定义， 同时也定义在这些类型是如何计算的。从这个观点上而言，m a r t i n l o f 类型理 论从构造数学发展而来，不承认任何的先验真值或者定义，是无假设条件的。 在定义一个新的类型时，可以使用已经在m a r t i n l o f 类型理论中已经定义 的类型，利用这些类型的计算方式来定义新的类型及其计算方式。从这个观点而 言，m a r ti n l o f 是相对有假设条件的。 m a r t i n l o f 类型理论采用集合的概念来定义其语法，在m a r t i n l o f 类型理 论的一开始就对集合进行了定义，并且解释了集合与命题、程序、证明之间的关 系。因此m a r t i n l o f 类型理论的意义是由计算来解释的，在此过程的第一步是 定义程序的语法以及它们是怎么样计算的。 2 2集合与命题、问题、程序的关系 m a r t i n l o f 类型理论起源于构造数学，但区别于绝大多数其他的数学形式 化，类型论不是基于一阶谓词演算。反过来，谓词逻辑通过命题和集合之间的对 应被解释于类型理论中。一个命题就是一个集合，其元素代表该命题的证明。因 此一个假命题被认为空集合以及一个真命题为非空集合。 在m a r t i n l o f 类型理论中，判断a a 至少能以下面的几种方式来理解： a 为集合a 中的一个元素 浙江大学硕士学位论文 a 为命题a 的一个证明 a 为满足规则说明a 的一个程序 a 为问题a 的一个解 这样做的原因是集合、命题、规则说明和问题这些概念能够以相同的方式来 解释。 2 2 1 命题与集合 在古典数学中，一个命题被认为真或假，独立于是否能够证明它或者反证它。 例如排中律a v ，a 在古典数学中是真，因为命题a 或者真或者假。在构造数学 中，一个命题被认为真或者假，取决于能够构造出这样的命题。因为没有证明或 者反正任意命题a 的方法，因此也没有办法判断a v 、a 的正确性。 这样，给出命题的构造解释是用证明而不是用独立于我们的数学对象世界。 首先考虑蕴含和合取操作。 ab 其一个证明是一个函数( 方法，程序) ，其对于a 的每个证明都给出b 的 一个证明。例如aoa ，给出一个方法，将输入变成输出。 x x 即是一个 证明。 a b 其一个证明是一个配对，它的第一个部分是a 的一个证明，而第二个部分 是b 的一个证明。若使用f s t 表示第一个部分，即f s t ( ) = a ，这里 是a 和b 的配对。那么九x f s t ( ) 是( a b ) a 的一个证明。 隐含在命题作为集合后面的思想是把命题等同于它的证明组成的集合。 那么一个命题为真指得是它得对应集合非空。以上解释得观点，对于蕴含和 合取可以得到： a b 等同于a b ，从a 至b 的函数结合。该集合中的元素为九x b ( x ) ， 当x a 时，b ( x ) b a b 等同于a b ，a 和b 的笛卡儿积。该集合中的元素为 ，这 里a e h 且b b 。 同样的道理，利用构造的思想来考虑谓词j 和v ，分析其与集合之间的关 系。 ( jx a ) b ( x ) 其一个证明是由集合a 的一个元素a 的一个构造以及b ( a ) 的一个证明而 组成。这样臼x a ) b ( x ) 的一个证明是一个配对 其中a 是集合a 的一个元素，并且b 为b ( a ) 的一个证明。此集合对应于一个集合族的不交 并，表示为( x a ) b ( x ) 。因此得到存在量词的解释如下：( 3x a ) b ( x ) 等同于( x a ) b ( x ) 。 浙江大学硕士学位论文 ( vx a ) b ( x ) 其个证明是一个函数( 方法，程序) ，其对于集合a 的每个元素a 给 定b ( a ) 的一个证明。对应于全称量词的集合是一族集合的笛卡儿积，表示 为n ( x a ) b ( x ) 。该集合中的元素是函数，当它作用于集合a 中的一个 元素时给出集合b ( a ) 的一个元素。因此( vx a ) b ( x ) 等同于集合兀( x a ) b ( x ) 2 2 2 命题与任务或者程序的规则说明 k o l m o g o r o v 。2 1 在1 9 3 2 年提出一个命题能够以下面的方式被解释为一个问题 或者一个任务。 若a 和b 为任务则 a b 为完成任务a 和b 的任务 avb 为完成至少是任务a 和b 之一的任务 a b 为在假设我们有a 的解答之下完成任务b 的任务。 他证明构造命题演算的规则被这个解释所证实。此解释能被用于说明程序的 任务如下： a b 是程序的规则说明，当程序执行时，得一个配对 ，这里a 是对 于任务a 的程序且b 是对于任务b 的程序。 avb 是程序的规则说明，当程序执行时，得i n l ( a ) 或者i n r ( b ) ，这里a 为a 的程序且b 为b 的程序。 a b 为程序的规则说明，当程序执行时，得xx b ( x ) ，这里在假设x 为a 的程序之下b ( x ) 为b 的程序。 此解释，能被推广到量词。 ( vx a ) b ( x ) 为程序的规则说明，当程序执行时，得 x b ( x ) ，这里在假 设x 为a 的对象之下b ( x ) 为b ( x ) 的程序。这是指当问题( vx a ) b ( x ) 的程序 作用于a 的任一对象x 时，结果得b ( x ) 的一个程序。 ( jx a ) b ( x ) 为程序的规则说明，当程序执行时，得 ，这里a 为a 的一个对象且b 为b ( a ) 的一个程序。这样，为了解释问题( jx a ) b ( x ) ，必须 找到一个方法其得a 的一个对象以及b ( a ) 的一个程序。 为了使此成为程序设计语言的规则说明语言，当然必须引入程序形式使得函 数能够作用于对象，使得能计算