论文部分内容阅读
面向服务的体系结构SOA (Service-Oriented Architeture)是一种新的分布式应用程序体系结构,它是构件重用和分布式技术发展的结果,业界提出将面向服务的体系结构作为软件体系结构下一个发展阶段来帮助IT组织应对所面临的越来越多的复杂性挑战。Web服务(Web Services)是当前实现SOA范型最有前景的技术。Web服务技术的广泛应用使得Web服务正逐步成为Internet网络环境中资源封装的标准形式。随着部署在Internet上的Web服务不断丰富,这些可被公共访问和集成的服务构成了一个潜在的巨大标准组件库。在Web服务互操作技术的基础上,提供高层的Web服务集成手段、实现Web服务组合成为Web服务技术发展的自然需求。总结当前的Web服务组合建模方法,主要分为语法方法、语义方法和形式化方法等。相对于其他服务组合方法,形式化建模方法有不可替代的重要作用。本论文从理论研究和实践结合两个方面着手,探索服务组合的形式化建模和验证技术。本论文的主要工作如下：1.建立了Web服务组合形式化模型,重点研究了用于描述Web服务交互过程的服务交互过程模型Web服务组合模型FMWSC (Formal Model for Web Service Composition)由两部分组成：服务描述模型、以及服务交互过程模型。服务描述模型基于Web服务描述语言WSDL (Web Services Description Language),用于描述Web服务组合的静态信息；服务交互过程模型用于描述Web服务的交互过程。Web服务交互过程模型能清晰表达Web服务组合中各组成部分之间的交互,并可模拟Web服务的交互过程,分析其动态性质。2.为了保证服务交互过程的正确性,给出了服务交互过程的形式化验证方法服务交互过程的形式化验证方法将模块化思想与模型验证技术相结合,即在对服务交互过程进行形式化验证时,重点验证服务基本交互过程。服务交互全过程的性质由这些基本过程的性质以及这些基本过程的组合方式所决定。采用这种方法的好处是可以有效地降低系统验证的规模,并提高验证的效率。验证的基本思路是：首先应用IMWSC模型的语义转换函数,将IMWSC描述转换为通信系统演算CCS表示,然后利用CWB-NC工具提供基于模态逻辑的检测机制对IMWSC模型实例进行验证。3.应用FMWSC建立了车辆维修管理系统模型,并应用本文提出的服务交互过程的验证机制对该系统的主要属性和行为一致性进行了验证以一个车辆维修管理系统VRMS (Vehicle Repair Management System)为例,详细介绍服务组合模型FMWSC的实际应用。首先给出组成VRMS系统的服务组件的静态描述,然后应用服务交互过程模型给出了(组成VRMS系统的)服务间的交互过程描述,并应用本文给出的服务交互过程模型的验证机制对该系统的主要属性和行为一致性进行了实际验证。在介绍CCML (Cooperative Computation Modeling Language)语言的基础上,给出了FMWSC模型与CCML语言的对应关系,并给出VRMS系统的(部分)CCML代码。