随着信息技术的发展，软件的规模不断扩大，如何保证和提高软件质量成为软件界最为关心的问题之一。软件测试作为保证软件质量的关键技术之一，能够有效地发现软件中的故障。据统计，在软件开发成本中，软件测试的工作量往往占软件开发总工作量的40％以上。对于某些安全关键的软件，其测试费用甚至高达所有其它软件工程阶段费用总和的三到五倍。因而，提高软件测试的有效性和测试效率、降低软件开发成本已成为软件工程师迫切需要解决的任务之一。 软件测试的核心问题是测试用例的产生。根据测试用例产生的依据可以将软件测试分为基于程序代码的测试和基于规格说明的测试两大类。基于程序代码的测试是指测试者根据程序的内部结构和与路径相关的数据特性设计测试用例。基于规格说明的测试是指测试者不需了解程序的内部结构，直接根据程序的需求规格说明来确定测试用例，推断测试结果的正确性。这种测试可以验证程序实现是否符合系统需求，从而实现软件测试的目的。同时，由于测试用例的开发是以系统规格说明为依据，测试用例的设计过程可以和程序开发过程同时进行，缩短了软件开发周期，提高了软件开发的效率。 形式化的软件规格说明具有精确的符号表示和清晰的语义，能够进行推理和证明，同时也便于工具的处理。因此，用形式化的规格说明作为测试用例的来源将会使得测试用例的自动构造成为可能。但目前基于形式规格说明构造测试用例的研究主要集中在利用黑盒测试准则(如：范畴划分测试准则，基于状态图的测试准则)从不同形式的规格说明(如：Z模式、UML状态图)中构造测试用例。但是对于基于模型的面向对象形式规格说明(如：Obiect-Z、VDM++规格说明)应用这些构造测试用例的技术非常困难。因为，这些基于模型的面向对象规格说明没有提供状态图，也很难将范畴划分测试准则应用到这些规格说明中用于定义输入空间的复杂谓词上。 本文提出了一系列用于从基于模型的面向对象形式规格说明推导测试用例的方法和技术。这些方法和技术分别探讨了在类测试层次以及类问测试层次上如何从基于模型的形式规格说明构造测试用例。在类测试层次上，本文定义了一个公理化系统对现有的可应用于方法内测试的逻辑覆盖准则进行评估，为测试人员从这组准则中选择某个准则提供了依据。此外，在这一层次的测试过程中，本文还提出了一组用于产生测试类的方法间交互的类内部测试准则。这组准则利用方法内测试用例来构造类内部测试用例，避免了以往的研究中采用基于状态图的测试准则构造测试用例时需要的抽取类的状态图的工作，使得机械化地构造类测试用例成为可能。在类间测试层次，本文给出了一系列用于测试类间的多态关系的上海大学工学博士学位论文测试准则，改变了以往对多态关系的测试主要集中于基于程序代码的方法。应用本文提出的这些用于测试类间多态关系的测试准则，测试人员可以从形式规格说明中推导出用于测试多态对象的测试用例，这些测试用例可以最终检测出程序代码中的多态关系的实现与规格说明中的定义是否一致。 除了给出若干个用于从基于模型的面向对象形式规格说明构造测试用例的测试准则之外，本文还提出了一个用于描述这种测试用例推导过程的测试框架。我们用形式规格说明语言objeet-Z来定义本文提出的测试框架。这样，测试框架的描述与规格说明的描述所采用的形式规格说明语言一致，从而避免了用另一种描述语言给读者带来的额外负担。本文对测试框架的阐述包括两个部分。第一部分是类测试框架。它用来描述类测试用例的推导过程，其中包括方法内测试用例、类内部测试用例、方法内测试用例的产生过程以及类内部测试用例推导过程的定义。第二部分包括如何利用类层次结构在子类中重用父类的类测试框架。利用本文提出的这个测试框架，测试用例生成系统在构造测试用例的同时可以自动记录测试用例生成过程，从而为测试用例的管理和追踪提供了方便。 最后，本文给出了一种应用求解线性规划和非线性不等式组对测试测试规格说明中定义的测试输入进行求解得到可以运行的具体的测试数据的方法，并且介绍一个实现了上述提出的测试技术的系统原型。