探索web服务组合形式化建模与验证研究

《探索web服务组合形式化建模与验证研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、大连海事大学博士学位论文Web服务组合形式化建模与验证研究姓名：包力申请学位级别：博士专业：交通信息工程及控制指导教师：张维石20091001中文摘要摘要面向服务的体系结构SOA(Service—OrientedArchiteture)是一种新的分布式应用程序体系结构，它是构件重用和分布式技术发展的结果，业界提出将面向服务的体系结构作为软件体系结构下一个发展阶段来帮助IT组织应对所面临的越来越多的复杂性挑战。Web服务(WebServices)是当前实现SOA范型最有前景的技术。web服务技术的广泛应用使得web服务jF逐步成为Inte

2、met网络环境中资源封装的标准形式。随着部署在Intemet上的web服务不断丰富，这些可被公共访问和集成的服务构成了一个潜在的巨大标准组件库。在Web服务互操作技术的基础上，提供高层的Web服务集成手段、实现Web服务组合成为Web服务技术发展的自然需求。总结当前的Web服务组合建模方法，主要分为语法方法、语义方法和形式化方法等。相对于其他服务组合方法，形式化建模方法有不可替代的重要作用。本论文从理沦研究和实践结合两个方面着手，探索服务组合的形式化建模和验证技术。本论文的主要工作如下：1．建立了web服务组合形式化模型，重点研究了用于

3、描述web服务交互过程的服务交互过程模型Web服务组合模型FMWSC(FormalModelforWebServiceComposition)由两部分组成：服务描述模型、以及服务交互过程模型。服务描述模型基于Web服务描述语言WSDL(WebServicesDescriptionLanguage)，用于描述Web服务组合的静态信息；服务交瓦过程模型用于描述wcb服务的交瓦过程。web服务交互过程模型能清晰表达web服务组合中各组成部分之间的交互，并可模拟Web服务的交互过程，分析其动态性质。2．为了保证服务交互过程的IF确性，给出了服务

4、交互过程的形式化验证方法．服务交互过程的形式化验征方法将模块化思想与模型验证技术相结合，即在对服务交互过程进行形式化验证时，重点验证服务基本交互过程。服务交互全过程的性质由这些基本过程的性质以及这些基本过程的组合方式所决定。采用这种中文摘要方法的好处是可以有效地降低系统验证的规模，并提高验证的效率。验证的基本思路是：首先应用IMWSC模型的语义转换函数，将IMWSC描述转换为通信系统演算CCS表示，然后利用CWB-NC工具提供基于模态逻辑的检测机制对IMWSC模型实例进行验证。3．应用FMWSC建立了车辆维修管理系统模型，并应用本文提出

5、的服务交互过程的验证机制对该系统的主要属性和行为一致性进行了验证以一个车辆维修管理系统VRMS(VehicleRepairManagementSystem)为例，详细介绍服务组合模型FMWSC的实际应用。首先给出组成VRMS系统的服务组件的静态描述，然后应用服务交互过程模型给出了(组成VRMS系统的)服务间的交互过程描述，并应用本文给出的服务交互过程模型的验证机制对该系统的主要属性和行为一致性进行了实际验证。在介绍CCML(CooperativeComputationModelingLanguage)语言的基础上，给出了FMWSC模型与

6、CCML语言的对应关系，并给出VRMS系统的(部分)CCML代码。关键词：Web服务组合；形式化方法；IMWSC模型；IM网模型；模型验证英文摘要AbstractRecently,Service—OrientedArchtecutre(SOAinshort)hasdrawnalotofattention．Itisakindofnewdistributedapplicationarchitectureandcomponenttechnology．SOAwhichcanhelpITorganizationsmeetmorechallengi

7、ngrequirementofmarketispromotedintheindustryasthenextevolutionarystepinsoftwarearchitecture．WebservicesarethemostpromisingtechniquetorealzeSOA．Webservicesaresoftwareapplicationswhichcanbeusedthroughanetwork(intranetorIntemet)viatheexchangeofmessagesbasedonXMLstandards．Du

8、etothelimitofthefunctionthatasinglewebserviceCanprovide，webservicesusuallyneedtobecomposedintolargerone