1。2  国内外研究现状

1。3  研究内容

本文叙述基于代数规约的Web服务自动化测试技术的相关理论，并在测试序列已生成的基础上，进行了自动化执行框架的整体设计及细节实现。

本文主要解决了现有的Web Service接口调用方式不统一的难点。

现有的Web Service实现方式主要是基于SOAP协议，数据格式采用WSDL。这种Web Service通常拥有自己的可视化服务接口，以及相应的接口信息描述。本文提出了以自动化测试工具Selenium为核心，通过将浏览器通信托管给Selenium的方式，调用可视化服务接口的框架。

目前流行的另一种Web Service实现方式是RESTful。RESTful是一种风格，而不是一组协议，也不是实现工具或框架。RESTful的主要思想是将Web Service作为一种可用URI唯一标识的资源，使用URI来调用。本文提出一个通过建立JAX-RS客户端的方式调用RESTful Web Service接口的框架。

1。4  本文档组织结构

本文共4章，本章节为引言，介绍背景、研究意义、研究内容、国内外研究现状等。其余各章主要内容如下：

第二章：介绍本文所提框架的理论基础，包括形式化方法基本概念，代数规约语言SOFIA基本语法，主流Web服务实现方式及调用方式，JAXB标准及相关组件，自动化测试工具Selenium等。

第三章：本文提出的测试执行框架的整体介绍，框架内部结构，例子介绍，实验环境搭建过程等内容。

第四章：用实验案例说明本文提出的测试执行框架的工作流程，主要内容为利用提出的调用框架实现测试用例执行，并给出关键部分代码。

2。  本课题涉及的原理与关键技术

2。1  形式化方法

形式化方法（Formal Methods），由于其基于数学的方法来描述目标软件系统属性，从而克服传统说明含糊、矛盾、不完整的缺点这样的本质，被发现适用于计算机科学和软件工程领域。人们期望形式化方法对软件和硬件系统的描述、开发和验证严谨的描述，可以像它应用于其它工程学科一样，提高软件设计的可靠性和鲁棒性（鲁棒即Robust，意思是健壮和强壮。描述系统在异常或危险情况下生存的能力）。

20世纪50年代后期，程序设计语言编译技术的研究催生了软件形式化方法，最早的为J。Backus提出的使用BNF描述的Algol60语言。从而将编译系统的开发，从简陋而效率低下的“传统手工业般制作方式”发展成拥有坚实理论基础的现代系统化方法。论文网

20世纪60年代后期爆发了“软件危机”（software crisis），为了解决“软件危机”,人们提出两类应对方法：一是在软件的开发过程中，弃用传统分散的管理方法，引进工程方法来组织、管理；二是在深入探讨程序开发生命周期（即程序开发过程）的规律基础上，提取统一的理论，并将其应用到实际的软件开发过程中来。第一类解决方法催生了“软件工程”及“软件开发工程化”的研究，而第二类解决方法则将人们的热情指向形式化方法的研究。之后30多年的相应研究与实际应用，为研究人员在形式化方法这一领域积累了很多重要成果。早期的有相对简单的形式化方法——一阶谓词演算方法，现在则发展到已经应用到不同领域的不同阶段的，基于代数的形式化方法。趋向完善的形式化方法也逐渐融入到软件开发生命周期的各个阶段中。

目前的形式化方法大致可以分为五类，各类的表达能力有所不同：

1）基于模型的方法：主要方式是对 作的明确定义，从而建 模型（主要形式是系统从 到另 的转换）。这种方法虽然对于表示 求（诸如时 求）很有效，但对于表 性并没有很好的办法。