基于形式方法面向服务的Web软件开发技术研究

论文摘要

网络技术的飞速发展,给人们的工作、生活方式带来了极大的变化,人们对网络的需求与依赖也越来越明显,对Web软件的需求也越来越多,例如电子政（商）务等。Web环境的开放性、分布性等特点使得Web软件开发方法不同于传统的软件开发方法。目前还没有很完善的Web软件开发方法。开发Web软件的方法基本上还是沿用传统的软件开发方法。传统的软件系统被开发为封闭的系统。虽然其构件可以来自外部,但合并到系统运行时,它们就在系统设计者控制之下。根据这一基本思想所开发的软件都具有这一特点。但在网络上,系统可能没有这样的集中控制,它们只在协议、地址和站点的交互上有统一标准,只在需要时动态绑定,所以需要一种允许用户利用网上自治的资源实现他们自己的组合,并能自动或人机互动进行服务的动态组装方法。基于Web的软件系统的建立和维护需要软件工程方法的进一步支持。为降低Web软件系统的设计开发难度,已经研究提出了基于软件体系结构、模型驱动等设计方法。这些方法的核心是模型的构造、模型的转换和精化。但目前软件体系结构以及模型驱动体系结构的建模语言主要是以UML作为标准建模语言。UML具有可视化、容易理解等特点,但缺乏严格的语义,而模型的转换必须建立在严格语义的基础上。本文提出基于形式方法面向服务的Web软件开发方法,围绕此问题分别从形式方法在面向服务构件的软件开发中的作用出发,对面向服务的软件体系结构的形式建模、基于模型的服务组合验证、基于形式本体的服务构件的发现、基于角色的设计模式形式建模及演化进行了研究。提出了基于面向服务软件体系结构的自顶向下的服务构件的组装理论。鉴于目前的面向服务软件体系结构的表示主要采用W3C给出的非形式化图形表示,不能精确表示软件结构的内涵,基于面向服务软件体系结构的服务构件自动化组装存在一定的难度。本文用形式规格说明语言Z对面向服务的软件体系结构进行了形式化,并提出把面向服务的软件体系结构作为一种风格来研究。面向服务的软件体系结构风格的形式化可以更为准确和方便地在体系结构的层次上进行交流。对不同的体系结构风格进行形式化描述,有利于系统的形式化验证和不同风格之间的比较。本文还分析定义了面向服务这样一种新出现的分布式软件体系结构风格的一些性质并给出了证明,并据此风格给出了一个应用实例,并对实例的活性进行了分析。服务组合是面向服务的Web软件开发的关键技术之一。如何有效地验证组合服务的功能及性能是服务组合研究中必须要解决的关键问题。为了能够自动地验证组合服务的各种属性,如组合服务是否能实现用户需求的功能,以及组合服务在运行过程中是否会出现用户不期望的行为,本文使用标签状态自动机建立组合服务的形式模型,将与用户的功能需求及期望的行为相关的性质表示为CTL公式,然后用形式验证工具SMV对服务组合进行了形式化验证。发现服务是面向服务Web软件开发中的另一关键技术。本文通过建立一个领域本体来扩展用户查询端查询的语义精确性,这种方法一方面可以提高服务构件的查准率和查全率。另一个好处是克服了其它基于语义的方法在实际服务查询中的可操作性方面的难度。我们的方法可以很好地利用已有的搜索引擎来达到对服务查询效能方面的提高,本文给出了一个服务搜索引擎的原型系统。体系结构反映系统的本质,由一些抽象的概念,以及概念间的关系来表示。但体系结构过于空泛,缺乏延伸性。设计模式正好可以弥补体系结构的这一缺陷,通过对体系结构的分析、分解,寻找和我们要解决问题匹配的模式可以使抽象的体系结构更接近用户熟悉的代码。本文提出了基于设计原则的设计模式选择方法,并给出了该方法的示例。针对目前的设计模式模型主要采用UML模型,缺乏明确语义,有些语义信息在UML图中难以反映出来的问题,本文利用形式规格说明语言Object-Z对设计模式建模,给出了基于角色的设计模式形式建模及演化方法与步骤,该方法可以避免模式在实例化时模式重叠、可追踪性差以及模式代码难于重用等问题,方便模式的自动化演化。最后,本文给出了面向服务的Web软件——BBS系统的开发实例,并就在面向服务的软件开发中如何使用设计模式进行了实践。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景
• 1.2 研究的内容及贡献
• 1.2.1 Web软件开发的软件体系结构模式问题
• 1.2.2 组合服务的验证问题
• 1.2.3 服务的发现问题
• 1.2.4 基于面向服务软件体系结构的模型演化问题
• 1.2.5 面向服务的软件开发技术应用问题
• 1.3 本文组织安排
• 第二章 相关技术概述
• 2.1 形式方法概述
• 2.1.1 形式方法的发展
• 2.1.2 形式方法的定义
• 2.1.3 形式方法的研究内容
• 2.1.4 形式方法的分类
• 2.2 模式的定义及分类
• 2.2.1 模式的定义
• 2.2.2 模式的类别
• 2.3 面向服务的体系结构模式
• 2.3.1 SOA的定义
• 2.3.2 SOA的特征
• 2.4 模型驱动的体系结构
• 第三章 形式化面向服务软件体系结构风格及分析
• 3.1 相关研究
• 3.2 形式规格说明语言-Z
• 3.2.1 Z语言概述
• 3.2.2 Z的组成
• 3.3 面向服务的软件体系结构风格建模
• 3.3.1 服务构件模型
• 3.3.2 服务连接器模型
• 3.3.3 系统配置模型
• 3.3.4 初始化配置模型
• 3.4 行为模型
• 3.5 匹配和组合模型
• 3.5.1 匹配
• 3.5.2 组合
• 3.6 分析
• 3.6.1 端口替换性分析
• 3.6.2 服务构件替换性分析
• 3.7 一个应用实例
• 3.8 小结
• 第四章 基于模型检测的Web服务组合验证
• 4.1 SMV模型检测工具介绍
• 4.2 基于标签有限自动机的Web服务行为模型
• 4.3 组合Web服务验证
• 4.4 基于模型验证组合Web服务的框架结构
• 4.5 小结
• 第五章 基于形式本体的服务发现研究
• 5.1 相关研究
• 5.2 本体及其创建
• 5.2.1 本体
• 5.2.2 本体的创建
• 5.3 相似性和相关性范畴
• 5.4 基于本体的服务查询方法
• 5.4.1 转换查询为RDF查询
• 5.4.2 查询求精和查询过程
• 5.5 系统实现
• 5.6 小结
• 第六章 基于角色的设计模式形式建模及演化
• 6.1 GOF设计模式概述
• 6.2 形式规格说明语言Object-Z
• 6.3 基于面向对象设计原则的设计模式选择
• 6.3.1 面向对象的设计原则
• 6.3.2 基于面向对象设计原则重构软件的设计过程
• 6.4 基于角色的设计模式形式建模
• 6.4.1 问题的提出
• 6.4.2 角色元模型
• 6.4.3 角色概念的形式化定义
• 6.4.4 设计模式形式化实例
• 6.5 设计模式演化及一致性验证
• 6.5.1 角色层演化
• 6.5.2 模式层演化
• 6.5.3 模式演化过程
• 6.5.4 一致性验证
• 6.6 小结
• 第七章 一个面向服务的WEb软件开发实例
• 7.1 系统概述
• 7.2 系统设计
• 7.3 系统中用到的设计模式
• 7.3.1 MVC设计模式
• 7.3.2 利用工厂模式控制业务对象的创建
• 7.3.3 利用单态模式控制对系统资源的访问
• 7.3.4 利用Java对迭代子模式的支持实现查询结果的显示
• 7.3.5 主题监测与观察者模式
• 7.4 小结
• 第八章 总结与展望
• 8.1 本文主要贡献
• 8.2 进一步的研究工作
• 参考文献
• 作者在攻读博士学位期间发表的论文
• 作者在攻读博士学位期间所参与的项目
• 致谢
• 附录1: 基于ONTOLOGY的搜索引擎实现代码
• 附录2: 面向服务的论坛系统源代码