2涉及的原理与关键技术
2.1形式化方法
基于模型为基础的规约的测试选择标准已经考虑在文学尤其是在Z符号族的上下文（例如 [Ammann 和 Offutt[22]]）。然而，使用的B法[Legeard[23]]，VDM[Dick和Faivre [24]]和方法的组合[Hierons[25]]也被考虑。这包括了基于分区的方法和其他方法和形式测试框架。许多系统有一个有限状态结构和有限状态机是一种自然的方式来描述这种结构。有限状态机定义一个比较差的语言在表现力和抽象的技术方面。然而，分析的有限状态机时缺乏表现力引入了一些显着的优势。很多问题是不可计算对于更一般的语言而对于有限状态机是可计算的，并经常可计算在低阶多项式次数。这有利于自动化测试序列生成。进程代数，如LOTOS，CCS和CSP，提供了一个优雅的形式化，专注于实体之间的通信。
目前，有很多的不同的方法去写出一个精确的规约。一种方法就是去建立一种预先设定的行为和语言的模型，诸如和Z，VDM和B做的一样，是通过描述可以与能改变状态的操作兼容的系统的状态。系统的状态使用设置，结果，关联和功能来描述，同时操作通过断定给定的前和后的条件来描述。有很多方法去构成一个规约。例如，Z中就用架构的一种语言做的，其中每个架构包含了声明断定哪种约束了架构。诸如Z，VDM和B这样基于模型的语言可以任意地描述通用的系统且有可能的无限状态。但是这样有一个缺陷，就是它使得推理较难实现自动化。然而，这个缺陷却不存在于有限状态规约语言中。正如其名称所体现的，以有限状态为基础的语言从一组有限的值来确定它们的状态，这往往用代表类似一个符号的操作的状态改变的状态转换来图形化表示，例如Z。这种语言的例子包括有限状态机（FSM ），SDL，状态图和X机。从这样的规格进行测试时基于有限状态机的测试技术已得到考虑。很多来自一个有限状态机测试软件的工作已经被协议一致性测试激发，因为有限状态机适用于指定通信协议的控制结构。然而，最近，以有限状态机为基础的测试已被内称为在其中一个模型被生成，以驱动测试基于模型的测试方法中使用。注意，术语“基于模型”被使用在不同的基于模型的测试和基于模型的规范语言中。并发性可以得到一个非常优雅的代数处理,且进程代数描述一个系统作为大量的通信的并发进程。基于有限状态的语言，如状态图和SDL也可以用来描述一个系统作为一组通信并发进程。然而，进程代数有丰富的理论，提供了实施关系的一致性的描述的替代概念。执行关系捕获几种类型的观察可以作出，除了迹线（输入和输出的序列）和环境的不同的属性。例如，CSP描述了一种系统作为通信并行运行的进程和事件同步的集合。
2.2代数规约及代数规约语言 SOFIA
代数规约测试显著的优点在于其可以自动产生测试用例和隐藏实现细节。
很多作者已经利用抽象数据类型（ADT）的代数规约和在面向对象（OO）的程序之间存在的并行。一个ADT是一个封装起来的数据与操作这些数据的操作的实体。在面向对象的程序中，类通过提供一个类的接口（其中列出的操作（或方法））和真正实现了操作的机体来构造。一个类也可以包含实例变量（或属性）中定义的类的对象的状态。ADT规格和接口类之间的相似性表明，形式化代数规约在测试面向对象软件有一个巨大的潜在作用。所采用的测试代数规约最早的工作是DAISTS系统的开发[Gannon[26]]，这也许并不奇怪，它利用了传统的结构测试标准版本。例如，为了增加用户自定义测试用例的彻底性的信息，DAISTS坚持，无论是公理和实现代码的每一部分被至少执行一次.该系统还结合一个较为复杂的表达式覆盖准则。这涉及“分离每个子表达式为公理和代码和报告这是从来没有评估或未能改变对所有评估”的任何表达 [Gannon[26]]。换句话说，该标准确保了所有的子表达式评价为两种不同的结果。 面向WEB服务的测试执行自动化技术框架设计与实现(3):http://www.751com.cn/jisuanji/lunwen_11982.html