在软件测试过程中，测试用例的生成是软件测试的关键和难点。目前，测试用例的生成主要靠手工完成，而且要求软件测试人员具有一定的经验和较高的专业水平，导致测试效率低下，软件成本居高不下，软件质量也很难保证。为此，迫切需要改进软件测试的方法，开发一些测试用例的自动生成工具，提高软件测试效率，降低软件成本，保证软件质量。 在以往的计算机科学中，对基于形式化规格的测试用例自动生成作了广泛的研究。但是软件测试和形式化方法之间往往存在着一定的鸿沟，测试人员通常怀疑形式化验证技术对实际问题的可应用性，而形式化方法的拥护者也无法接受通过充分测试技术来产生正确的软件。传统形式化语言的一个缺点就是要求使用者有较扎实的数学基础，不适合普通的系统建模人员的使用。 本文介绍了对象约束语言(OCL)在实际建模中的应用，并且形式化描述了OCL的语法及语义。OCL是一种对UML模型进行约束描述的形式化语言，允许开发人员创建模型中各个对象之间的详细约束规则。 我们阐述了一种基于前置和后置规格说明的缺陷测试用例生成技术。基于测试用例的形式定义，介绍了测试用例生成算法的理论以及如何将该算法转化为约束满足问题(CSP)的求解。 本文提出一种新型的OCL规格变异系统的设计方案，并详细描述了一些变异算子的具体实现。解决了传统变异系统的性能缺陷，提高了变异分析的实用性。本文介绍了对类的单个方法进行自动划分分析以及对给定类方法构造有效的测试序列的方法。利用Choco约束编程系统，将测试用例生成算法建模为一个约束满足问题，通过求解约束满足问题来生成单元测试用例集。 为了证明上述理论和方法的可行性，我们开发了一个基于UML、OCL规格单元测试用例的自动生成工具原型。我们希望通过一种新的基于形式化方法的测试用例自动生成技术在形式化方法和软件测试之间架起一座桥梁，缩小两者之间的差距，从而提高软件的生产效率。