毕业论文移动版

2）基于逻辑的方法：主要思想是用逻辑的方法描述系统预期的性能（系统性能包括时序、底层规约和可能的行为）。主要形式是使用公理系统（与所选逻辑相关）证明系统是否达到预期的性能。

3）代数方法：主要思想为将未定义状态下不同的操作行为联系起来，主要做法是给出操作的显式定义。与基于模型的方法类似，代数方法并不能显式表示并发状态。

4）过程代数方法：主要思想为限制所有容许的可观察的过程，并用它们之间的通信表示系统行为。过程代数方法支持显式表示并发过程。

5）基于网络的方法：主要思想是使用具有形式语义的图形语言描述系统。因为图形化表示法易于理解，而且非专业人员能够使用，因此使系统确定表示法被广泛应用于开发过程中。

2。2  代数规约语言

20世纪70年代，代数规约技术开始出现，它采用独立于实现的方式定义抽象数据类型，用公理集的方式描述抽象数据类型的约束。基于代数规约的测试方法，由于其设计与实现独立于软件系统，且在自动生成测试用例、提供测试驱动和判断测试输出等方面有独到之处，已经被研究人员应用于测试工作。可以测试的对象有：抽象数据类型、类、过程、Web服务和组件等[8]。

代数规约由数个软件实体集构成（抽象数据类型、类、服务，甚至现实世界中的物理对象、数据、过程等，都可以视为软件实体），软件实体由规约单元描述。这样的话，一个描述Web Service的代数规约就可分解为数个规约单元。规约单元用Sort描述，Sort也被称为类子，是规约单元的唯一的标识。类子包括基调（Signature）、公理集（Axiom）两部分。基调为定义在类子上的操作集（Operators），公理集为操作的语义约束。此外，新的规约单元可以通过扩展（extends）和使用（uses）两种方式重用已有的规约单元。

本文所构建的测试执行框架所使用的代数规约语言为SOFIA语言。

SOFIA语言拥有之前提到的代数规约语言的共有特点，整体结构为一组规约单元，而规约单元分为两个部分：基调单元（Signature）和公理单元（Axiom）。此外，SOFIA的规约单元还有定义（Definition）部分，用户可以在此部分定义规约的辅助函数和概念。下面以Stack服务为例介绍SOFIA语言。

Stack服务提供简单的堆栈服务，操作有PUSH、POP、REPLACE。

Spec StackService;

uses  PushRequest, PopRequest,ReplaceRequest,

      PushResponse, PopResponse,ReplaceResponse,

Integer,Bool;

Const:nil;

Attr

   isEmpty:Bool;

   length: Integer;

   top: Integer;

Operation

push(PushRequest): PushResponse;

pop(PopRequest):PopResponse;

replace(ReplaceRequest): ReplaceResponse;

Axiom

   nil。isEmpty = True;

   nil。length = 0;

For all S : StackService ,X : PopRequest that

   S。isEmpty = True, if  S。length = 0;

   S;pop(X)。length = S。length-1, if S。length>0;

End

For all S : StackService, X: PushRequest that

   S;push(X)。isEmpty = False;

   S;push(X)。top = X。value;

   S;push(X)。length = S。length+1;

End

For all S : StackService, X : ReplaceRequest that

   S;replace(X)。top = X。value, if S。length>0;

EndEnd

Spec为SOFIA语言的基本语句段，相对于代数规约的规约单元。Uses部分描述本规约单元用到的数据类型，可以为基本数据类型，如integer、bool，也可以为复杂数据类型，如PushRequest（PUSH操作的请求信息）。Const部分描述本规约单元使用的固定部分，nil表示栈的初始状态（空栈）。Attr可以简单的理解为局部变量。Operation描述规约单元的操作集，在此规约单元中包括PUSH、POP、REPLACE操作。push(PushRequest): PushResponse表示push操作以PushRequest为输入，PushResponse为返回。Axiom描述操作的语义约束。Axiom的BNF（Backus-Naur Form）表示为：文献综述 (责任编辑：qin)