面向对象技术作为一种全新的软件工程思想，在软件开发中的广泛使用。但是其独有的封装、继承、多态等特性，使得传统的软件测试技术已经不能够有效地完成测试。因此测试策略和测试方法都需要进行相应的改进。 形式化方法是基于数学方法来描述目标软件系统性质的软件开发方法，它为系统说明、开发和验证提供了一个框架。Object-Z是一种形式规格说明语言，其基础是Z语言。用Obiect-Z来描述面向对象软件规格说明，具有简明、精确、无二义性的优点。 Harrold和Rothermel将类的单元测试分成三个级别：方法内测试、方法间测试和类内部测试。Stock和Carrington提出的基于形式化规格说明的测试模板框架TTF(Test Template Framework)，可以在详细设计阶段就生成类测试用例，但生成的测试模板只能完成方法内和方法间测试，而无法判断测试模板序列执行后，类内部状态的正确性，即无法完成类内部测试。 本文提出的基于形式规格说明的类测试框架是针对TIT框架在类状态测试方面的扩展。主要思想：首先，利用TTF框架生成的方法测试模板构造类的有限状态自动机。其中，构造过程分为状态推导和迁移规则推导两个步骤；然后，生成测试模板所有可能的调用序列，即测试路径生成；最后，根据测试路径构造测试类的集合，每个测试类是一个Obiect-Z描述的类模式。 扩展后的ETTF框架不仅可以完成对类内部方法的测试，并且可以考察类内部状态改变的正确性，达到完整的单元测试的目的。同时，由于测试用例是从Object-Z规格说明推导出的，而且整体推导过程也是一个形式化的过程，因此提高了测试的可靠性和有效性。